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

Theorem pm2.21 547
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 545 1 φ → (φψ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-in2 545
This theorem is referenced by:  pm2.21d  549  pm2.24  551  pm2.24i  553  pm2.21i  575  pm2.52  582  jarl  584  mtt  610  orel2  645  imorri  668  pm2.42  694  pm2.18dc  750  simplimdc  757  peircedc  820  pm4.82  857  pm5.71dc  868  dedlemb  877  mo2n  1928  exmodc  1950  exmonim  1951  nrexrmo  2523  opthpr  3537  0neqopab  5495  0mnnnnn0  8082
  Copyright terms: Public domain W3C validator