let p, q, r be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- p => q & X |- q => r holds
X |- p => r
let X be Subset of LTLB_WFF; :: thesis: ( X |- p => q & X |- q => r implies X |- p => r )
assume that
A1: X |- p => q and
A2: X |- q => r ; :: thesis: X |- p => r
set A = (p => q) => ((q => r) => (p => r));
now :: thesis: for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . ((p => q) => ((q => r) => (p => r))) = 1
let f be Function of LTLB_WFF,BOOLEAN; :: thesis: (VAL f) . ((p => q) => ((q => r) => (p => r))) = 1
thus (VAL f) . ((p => q) => ((q => r) => (p => r))) = ((VAL f) . (p => q)) => ((VAL f) . ((q => r) => (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((VAL f) . ((q => r) => (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => (((VAL f) . (q => r)) => ((VAL f) . (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => ((VAL f) . r)) => ((VAL f) . (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => ((VAL f) . r)) => (((VAL f) . p) => ((VAL f) . r))) by Def15
.= 1 by XBOOLEAN:106 ; :: thesis: verum
end;
then (p => q) => ((q => r) => (p => r)) is LTL_TAUT_OF_PL ;
then (p => q) => ((q => r) => (p => r)) in LTL_axioms by Def17;
then X |- (p => q) => ((q => r) => (p => r)) by Th42;
then X |- (q => r) => (p => r) by A1, Th43;
hence X |- p => r by A2, Th43; :: thesis: verum