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

now

let f be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL f) . ((p => (q => r)) => ((r => s) => (p => (q => s)))) = 1
A3: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def 3;
A4: ( (VAL f) . r = 0 or (VAL f) . r = 1 ) by XBOOLEAN:def 3;
set B = (VAL f) . (p => (q => r));
set C = (VAL f) . (r => s);
set D = (VAL f) . (p => (q => s));
A5: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def 3;
A6: ( (VAL f) . s = 0 or (VAL f) . s = 1 ) by XBOOLEAN:def 3;
A7: (VAL f) . (p => (q => s)) = ((VAL f) . p) => ((VAL f) . (q => s)) by Def16
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . s)) by Def16 ;
A8: (VAL f) . (p => (q => r)) = ((VAL f) . p) => ((VAL f) . (q => r)) by Def16
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r)) by Def16 ;
thus (VAL f) . ((p => (q => r)) => ((r => s) => (p => (q => s)))) = ((VAL f) . (p => (q => r))) => ((VAL f) . ((r => s) => (p => (q => s)))) by Def16
.= ((VAL f) . (p => (q => r))) => (((VAL f) . (r => s)) => ((VAL f) . (p => (q => s)))) by Def16
.= 1 by A3, A5, A4, A6, A8, A7, Def16 ; :: thesis: verum

end;

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