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 :: thesis: for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . ((p => (q => r)) => ((r => s) => (p => (q => s)))) = 1

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 Def15
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . s)) by Def15 ;
A8: (VAL f) . (p => (q => r)) = ((VAL f) . p) => ((VAL f) . (q => r)) by Def15
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r)) by Def15 ;
thus (VAL f) . ((p => (q => r)) => ((r => s) => (p => (q => s)))) = ((VAL f) . (p => (q => r))) => ((VAL f) . ((r => s) => (p => (q => s)))) by Def15
.= ((VAL f) . (p => (q => r))) => (((VAL f) . (r => s)) => ((VAL f) . (p => (q => s)))) by Def15
.= 1 by A3, A5, A4, A6, A8, A7, Def15 ; :: thesis: verum

end;

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