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