let p, q, r be boolean object ; :: thesis: ( p => q = TRUE implies (q => r) => (p => r) = TRUE )
( r = FALSE or r = TRUE ) by Def3;
hence ( p => q = TRUE implies (q => r) => (p => r) = TRUE ) ; :: thesis: verum