Theorem pm2.21 612

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-in2 610

This theorem is referenced by:  pm2.21d  614  pm2.24  616  pm2.24i  618  pm2.21i  641  jarl  653  mtt  680  orel2  721  imorri  744  pm2.42  772  pm2.18dc  850  simplimdc  855  peircedc  909  pm4.82  945  pm5.71dc  956  dedlemb  965  mo2n  2047  exmodc  2069  exmonim  2070  nrexrmo  2686  opthpr  3759  0neqopab  5898  0mnnnnn0  9167  flqeqceilz  10274