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

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 Def16
.= (((VAL f) . p) => ((VAL f) . (q => r))) => ((VAL f) . ((p '&&' q) => r)) by Def16
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((VAL f) . ((p '&&' q) => r)) by Def16
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => (((VAL f) . (p '&&' q)) => ((VAL f) . r)) by Def16
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) by Th32
.= 1 by Th3 ; :: thesis: verum

end;

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