let A, B, C be Element of LTLB_WFF ; :: thesis: (A => (B => C)) => ((A => B) => (A => C)) is LTL_TAUT_OF_PL
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . ((A => (B => C)) => ((A => B) => (A => C))) = 1
set v = VAL g;
A1: ( (VAL g) . A = 1 or (VAL g) . A = 0 ) by XBOOLEAN:def 3;
A2: ( (VAL g) . B = 1 or (VAL g) . B = 0 ) by XBOOLEAN:def 3;
A3: ( (VAL g) . C = 1 or (VAL g) . C = 0 ) by XBOOLEAN:def 3;
thus (VAL g) . ((A => (B => C)) => ((A => B) => (A => C))) = ((VAL g) . (A => (B => C))) => ((VAL g) . ((A => B) => (A => C))) by LTLAXIO1:def 15
.= (((VAL g) . A) => ((VAL g) . (B => C))) => ((VAL g) . ((A => B) => (A => C))) by LTLAXIO1:def 15
.= (((VAL g) . A) => (((VAL g) . B) => ((VAL g) . C))) => ((VAL g) . ((A => B) => (A => C))) by LTLAXIO1:def 15
.= (((VAL g) . A) => (((VAL g) . B) => ((VAL g) . C))) => (((VAL g) . (A => B)) => ((VAL g) . (A => C))) by LTLAXIO1:def 15
.= (((VAL g) . A) => (((VAL g) . B) => ((VAL g) . C))) => ((((VAL g) . A) => ((VAL g) . B)) => ((VAL g) . (A => C))) by LTLAXIO1:def 15
.= 1 by ; :: thesis: verum