let p, q, r be Element of PL-WFF ; :: thesis: (p => q) => ((p => r) => (p => (q '&' r))) is tautology
let M be PLModel; :: according to PL_AXIOM:def 18 :: thesis: (SAT M) . ((p => q) => ((p => r) => (p => (q '&' r)))) = 1
thus (SAT M) . ((p => q) => ((p => r) => (p => (q '&' r)))) = ((SAT M) . (p => q)) => ((SAT M) . ((p => r) => (p => (q '&' r)))) by Def11
.= (((SAT M) . p) => ((SAT M) . q)) => ((SAT M) . ((p => r) => (p => (q '&' r)))) by Def11
.= (((SAT M) . p) => ((SAT M) . q)) => (((SAT M) . (p => r)) => ((SAT M) . (p => (q '&' r)))) by Def11
.= (((SAT M) . p) => ((SAT M) . q)) => ((((SAT M) . p) => ((SAT M) . r)) => ((SAT M) . (p => (q '&' r)))) by Def11
.= (((SAT M) . p) => ((SAT M) . q)) => ((((SAT M) . p) => ((SAT M) . r)) => (((SAT M) . p) => ((SAT M) . (q '&' r)))) by Def11
.= (((SAT M) . p) => ((SAT M) . q)) => ((((SAT M) . p) => ((SAT M) . r)) => (((SAT M) . p) => (((SAT M) . q) '&' ((SAT M) . r)))) by semcon2
.= 1 by th5 ; :: thesis: verum