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