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