Theorem pm2.21 618

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by Mario Carneiro, 12-May-2015.)

Assertion

Ref	Expression
pm2.21	⊢ (¬ 𝜑 → (𝜑 → 𝜓))

Proof of Theorem pm2.21

Step	Hyp	Ref	Expression
1		ax-in2 616	1 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-in2 616

This theorem is referenced by:  pm2.21d  620  pm2.24  622  pm2.24i  624  pm2.21i  647  jarl  659  mtt  686  orel2  727  imorri  750  pm2.42  778  pm2.18dc  856  simplimdc  861  peircedc  915  pm4.82  951  pm5.71dc  962  dedlemb  971  mo2n  2064  exmodc  2086  exmonim  2087  nrexrmo  2704  opthpr  3784  0neqopab  5933  0mnnnnn0  9222  flqeqceilz  10332