NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm2.21 GIF version

Theorem pm2.21 100
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 NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)
Assertion
Ref Expression
pm2.21 φ → (φψ))

Proof of Theorem pm2.21
StepHypRef Expression
1 id 19 . 2 φ → ¬ φ)
21pm2.21d 98 1 φ → (φψ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.24  101  pm2.18  102  notnot2  104  simplim  143  jarl  155  orel2  372  pm2.42  557  pm4.82  894  pm5.71  902  dedlem0b  919  dedlemb  921  dfnot  1332  cad0  1400  meredith  1404  tbw-bijust  1463  tbw-negdf  1464  ax12dgen2  1726  19.38  1794  nfimdOLD  1809  hbimdOLD  1816  hbimOLD  1818  a16g  1945  sbi2  2064  ax46to6  2164  ax467to6  2171  ax467to7  2172  ax11indi  2196  mo  2226  mo2  2233  exmo  2249  2mo  2282  nrexrmo  2828  elab3gf  2990  moeq3  3013  pwadjoin  4119  dff3  5420
  Copyright terms: Public domain W3C validator