Theorem pm2.21 620

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-in2 618

This theorem is referenced by:  pm2.21d  622  pm2.24  624  pm2.24i  626  pm2.21i  649  jarl  662  mtt  689  orel2  731  imorri  754  pm2.42  782  pm2.18dc  860  simplimdc  865  peircedc  919  pm4.82  956  pm5.71dc  967  dedlemb  976  mo2n  2105  exmodc  2128  exmonim  2129  nrexrmo  2753  opthpr  3849  0neqopab  6040  0mnnnnn0  9389  flqeqceilz  10527