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

Theorem pm2.21 580
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 578 1 𝜑 → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-in2 578
This theorem is referenced by:  pm2.21d  582  pm2.24  584  pm2.24i  586  pm2.21i  608  pm2.52  615  jarl  617  mtt  643  orel2  678  imorri  701  pm2.42  727  pm2.18dc  784  simplimdc  791  peircedc  854  pm4.82  892  pm5.71dc  903  dedlemb  912  mo2n  1971  exmodc  1993  exmonim  1994  nrexrmo  2576  opthpr  3585  0neqopab  5603  0mnnnnn0  8464  flqeqceilz  9477
  Copyright terms: Public domain W3C validator