let p, q, r be boolean object ; :: thesis: (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE

A1: ( q = FALSE or q = TRUE ) by Def3;

A2: ( p = FALSE or p = TRUE ) by Def3;

( r = FALSE or r = TRUE ) by Def3;

hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE by A1, A2; :: thesis: verum

A1: ( q = FALSE or q = TRUE ) by Def3;

A2: ( p = FALSE or p = TRUE ) by Def3;

( r = FALSE or r = TRUE ) by Def3;

hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) = TRUE by A1, A2; :: thesis: verum