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