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  841  simplimdc  846  peircedc  900  pm4.82  935  pm5.71dc  946  dedlemb  955  mo2n  2028  exmodc  2050  exmonim  2051  nrexrmo  2650  opthpr  3707  0neqopab  5824  0mnnnnn0  9033  flqeqceilz  10122