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