<neg

Theorem. From a wff and its negation, anything is true.

Description:

Theorem *2.21 of Principia Mathematica, p. 104; pm2.21 in set.mm. Also called the Duns Scotus law.

Arguments:

phi (pr), psi (pr),

Assertions:

(lnotphito(phitopsi))

Proof:

Hyp Ref Line Expr
ax11(lnotphito(lnotpsitolnotphi))
1ax32(lnotphito(phitopsi))