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

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 Def16
.= (((VAL f) . (p '&&' q)) => ((VAL f) . r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Def16
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Th32
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . (p => s)) => ((VAL f) . ((p '&&' q) => (s '&&' r)))) by Def16
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => ((VAL f) . ((p '&&' q) => (s '&&' r)))) by Def16
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => (((VAL f) . (p '&&' q)) => ((VAL f) . (s '&&' r)))) by Def16
.= ((((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 Th32
.= 1 by A3, A4, A6, A5, Th32 ; :: thesis: verum

end;

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