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  2034  exmodc  2056  exmonim  2057  nrexrmo  2673  opthpr  3735  0neqopab  5866  0mnnnnn0  9122  flqeqceilz  10217