Theorem pm2.21 622

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 620	1 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-in2 620

This theorem is referenced by:  pm2.21d  624  pm2.24  626  pm2.24i  628  pm2.21i  651  jarl  664  mtt  692  orel2  734  imorri  757  pm2.42  785  pm2.18dc  863  simplimdc  868  peircedc  922  pm4.82  959  pm5.71dc  970  dedlemb  979  mo2n  2107  exmodc  2130  exmonim  2131  nrexrmo  2756  opthpr  3860  0neqopab  6076  0mnnnnn0  9477  flqeqceilz  10624