ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21 GIF version

Theorem pm2.21 612
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
StepHypRef Expression
1 ax-in2 610 1 𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-in2 610
This theorem is referenced by:  pm2.21d  614  pm2.24  616  pm2.24i  618  pm2.21i  641  jarl  653  mtt  680  orel2  721  imorri  744  pm2.42  772  pm2.18dc  850  simplimdc  855  peircedc  909  pm4.82  945  pm5.71dc  956  dedlemb  965  mo2n  2047  exmodc  2069  exmonim  2070  nrexrmo  2686  opthpr  3759  0neqopab  5898  0mnnnnn0  9167  flqeqceilz  10274
  Copyright terms: Public domain W3C validator