con

Theorem. Contraposition.

Description:

Theorem *2.16 of Principia Mathematica, p. 103; con3 in set.mm.

Arguments:

phi (pr), psi (pr),

Assertions:

((phitopsi)to(lnotpsitolnotphi))

Proof:

Hyp Ref Line Expr
neg>1(psitolnotlnotpsi)
1syl<2((phitopsi)to(phitolnotlnotpsi))
2con>3((phitopsi)to(lnotpsitolnotphi))