let p, q, r be Element of LTLB_WFF ; :: thesis: (p => q) => ((p => ('not' r)) => (p => ('not' (q => r)))) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . ((p => q) => ((p => ('not' r)) => (p => ('not' (q => r))))) = 1
set v = VAL g;
A1: ( (VAL g) . r = 1 or (VAL g) . r = 0 ) by XBOOLEAN:def 3;
A2: ( (VAL g) . q = 1 or (VAL g) . q = 0 ) by XBOOLEAN:def 3;
A3: (VAL g) . ((p => ('not' r)) => (p => ('not' (q => r)))) = ((VAL g) . (p => ('not' r))) => ((VAL g) . (p => ('not' (q => r)))) by LTLAXIO1:def 15
.= (((VAL g) . p) => ((VAL g) . ('not' r))) => ((VAL g) . (p => ('not' (q => r)))) by LTLAXIO1:def 15
.= (((VAL g) . p) => ((VAL g) . ('not' r))) => (((VAL g) . p) => ((VAL g) . ('not' (q => r)))) by LTLAXIO1:def 15
.= (((VAL g) . p) => (((VAL g) . r) => ((VAL g) . TFALSUM))) => (((VAL g) . p) => ((VAL g) . ('not' (q => r)))) by LTLAXIO1:def 15
.= (((VAL g) . p) => (((VAL g) . r) => ((VAL g) . TFALSUM))) => (((VAL g) . p) => (((VAL g) . (q => r)) => ((VAL g) . TFALSUM))) by LTLAXIO1:def 15
.= (((VAL g) . p) => (((VAL g) . r) => ((VAL g) . TFALSUM))) => (((VAL g) . p) => ((((VAL g) . q) => ((VAL g) . r)) => ((VAL g) . TFALSUM))) by LTLAXIO1:def 15 ;
A4: ( (VAL g) . TFALSUM = 0 & (VAL g) . (p => q) = ((VAL g) . p) => ((VAL g) . q) ) by LTLAXIO1:def 15;
( (VAL g) . p = 1 or (VAL g) . p = 0 ) by XBOOLEAN:def 3;
hence (VAL g) . ((p => q) => ((p => ('not' r)) => (p => ('not' (q => r))))) = 1 by A1, A2, A4, LTLAXIO1:def 15, A3; :: thesis: verum