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) => ((VAL f) . (q => r))) => ((VAL f) . ((p '&&' q) => r)) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((VAL f) . ((p '&&' q) => r)) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => (((VAL f) . (p '&&' q)) => ((VAL f) . r)) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) by Th31
.= 1 by Th2 ; :: 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