Description: Inference associated with con4 . Its associated inference is mt4 .

Remark: this can also be proved using notnot followed by nsyl2 ,
giving a shorter proof but depending on more axioms (namely, ax-1 and
ax-2 ). (Contributed by NM, 29-Dec-1992)