Theorem pm2.21 607

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-in2 605

This theorem is referenced by:  pm2.21d  609  pm2.24  611  pm2.24i  613  pm2.21i  636  jarl  648  mtt  675  orel2  716  imorri  739  pm2.42  767  pm2.18dc  845  simplimdc  850  peircedc  904  pm4.82  940  pm5.71dc  951  dedlemb  960  mo2n  2042  exmodc  2064  exmonim  2065  nrexrmo  2682  opthpr  3752  0neqopab  5887  0mnnnnn0  9146  flqeqceilz  10253