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

proof

let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL f) . ((r => (p '&&' q)) => (r => p)) = 1
thus (VAL f) . ((r => (p '&&' q)) => (r => p)) = ((VAL f) . (r => (p '&&' q))) => ((VAL f) . (r => p)) by Def15
.= (((VAL f) . r) => ((VAL f) . (p '&&' q))) => ((VAL f) . (r => p)) by Def15
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => ((VAL f) . (r => p)) by Th31
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => (((VAL f) . r) => ((VAL f) . p)) by Def15
.= 1 by Th1 ; :: thesis: verum

end;

then (r => (p '&&' q)) => (r => p) in LTL_axioms by Def17;
then X |- (r => (p '&&' q)) => (r => p) by Th42;
hence X |- r => p by A1, Th43; :: thesis: X |- r => q
set A = (r => (p '&&' q)) => (r => q);
(r => (p '&&' q)) => (r => q) is LTL_TAUT_OF_PL

proof

let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL f) . ((r => (p '&&' q)) => (r => q)) = 1
thus (VAL f) . ((r => (p '&&' q)) => (r => q)) = ((VAL f) . (r => (p '&&' q))) => ((VAL f) . (r => q)) by Def15
.= (((VAL f) . r) => ((VAL f) . (p '&&' q))) => ((VAL f) . (r => q)) by Def15
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => ((VAL f) . (r => q)) by Th31
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => (((VAL f) . r) => ((VAL f) . q)) by Def15
.= 1 by Th1 ; :: thesis: verum

end;

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