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)));

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

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

then
(p => (q => r)) => ((r => s) => (p => (q => s))) is LTL_TAUT_OF_PL
;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;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

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