let p, q, r be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- (p '&&' q) => r holds
X |- p => (q => r)
let X be Subset of LTLB_WFF; :: thesis: ( X |- (p '&&' q) => r implies X |- p => (q => r) )
set A = ((p '&&' q) => r) => (p => (q => r));

now :: thesis: for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . (((p '&&' q) => r) => (p => (q => r))) = 1

let f be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL f) . (((p '&&' q) => r) => (p => (q => r))) = 1
thus (VAL f) . (((p '&&' q) => r) => (p => (q => r))) = ((VAL f) . ((p '&&' q) => r)) => ((VAL f) . (p => (q => r))) by Def15
.= (((VAL f) . (p '&&' q)) => ((VAL f) . r)) => ((VAL f) . (p => (q => r))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((VAL f) . (p => (q => r))) by Th31
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . p) => ((VAL f) . (q => r))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) by Def15
.= 1 by Th3 ; :: thesis: verum

end;

then ((p '&&' q) => r) => (p => (q => r)) is LTL_TAUT_OF_PL ;
then ((p '&&' q) => r) => (p => (q => r)) in LTL_axioms by Def17;
then A1: X |- ((p '&&' q) => r) => (p => (q => r)) by Th42;
assume X |- (p '&&' q) => r ; :: thesis: X |- p => (q => r)
hence X |- p => (q => r) by A1, Th43; :: thesis: verum