let p, q, r be Element of LTLB_WFF ; :: thesis: (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms
(p => (q => r)) => ((p => q) => (p => r)) is LTL_TAUT_OF_PL

proof

let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL f) . ((p => (q => r)) => ((p => q) => (p => r))) = 1
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def 3;
A2: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def 3;
A3: ( (VAL f) . r = 0 or (VAL f) . r = 1 ) by XBOOLEAN:def 3;
thus (VAL f) . ((p => (q => r)) => ((p => q) => (p => r))) = ((VAL f) . (p => (q => r))) => ((VAL f) . ((p => q) => (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . (q => r))) => ((VAL f) . ((p => q) => (p => r))) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((VAL f) . ((p => q) => (p => r))) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => (((VAL f) . (p => q)) => ((VAL f) . (p => r))) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((((VAL f) . p) => ((VAL f) . q)) => ((VAL f) . (p => r))) by Def15
.= 1 by A1, A2, A3, Def15 ; :: thesis: verum

end;

hence (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms by Def17; :: thesis: verum