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

Theorem pm2.21 606
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 604 1 𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-in2 604
This theorem is referenced by:  pm2.21d  608  pm2.24  610  pm2.24i  612  pm2.21i  635  jarl  647  mtt  674  orel2  715  imorri  738  pm2.42  766  pm2.18dc  840  simplimdc  845  peircedc  899  pm4.82  934  pm5.71dc  945  dedlemb  954  mo2n  2027  exmodc  2049  exmonim  2050  nrexrmo  2647  opthpr  3699  0neqopab  5816  0mnnnnn0  9016  flqeqceilz  10098
  Copyright terms: Public domain W3C validator