Theorem pm2.21 606

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-in2 604

This theorem is referenced by:  pm2.21d  608  pm2.24  610  pm2.24i  612  pm2.21i  635  jarl  647  mtt  674  orel2  715  imorri  738  pm2.42  766  pm2.18dc  840  simplimdc  845  peircedc  899  pm4.82  934  pm5.71dc  945  dedlemb  954  mo2n  2025  exmodc  2047  exmonim  2048  nrexrmo  2645  opthpr  3694  0neqopab  5809  0mnnnnn0  9002  flqeqceilz  10084