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

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

let f be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL f) . (((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r)))) = 1
A3: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def 3;
A4: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def 3;
A5: ( (VAL f) . s = 0 or (VAL f) . s = 1 ) by XBOOLEAN:def 3;
A6: ( (VAL f) . r = 0 or (VAL f) . r = 1 ) by XBOOLEAN:def 3;
thus (VAL f) . (((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r)))) = ((VAL f) . ((p '&&' q) => r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Def15
.= (((VAL f) . (p '&&' q)) => ((VAL f) . r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Th31
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . (p => s)) => ((VAL f) . ((p '&&' q) => (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => ((VAL f) . ((p '&&' q) => (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => (((VAL f) . (p '&&' q)) => ((VAL f) . (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . (s '&&' r)))) by Th31
.= 1 by A3, A4, A6, A5, Th31 ; :: thesis: verum

end;

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