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  660  mtt  687  orel2  728  imorri  751  pm2.42  779  pm2.18dc  857  simplimdc  862  peircedc  916  pm4.82  953  pm5.71dc  964  dedlemb  973  mo2n  2083  exmodc  2105  exmonim  2106  nrexrmo  2728  opthpr  3815  0neqopab  5997  0mnnnnn0  9334  flqeqceilz  10470