Theorem pm2.21 124

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (The proof was shortened by Wolf Lammen, 14-Sep-2012.)

Assertion

Ref	Expression
pm2.21	|- (-. ph -> (ph -> ps))

Proof of Theorem pm2.21

Step	Hyp	Ref	Expression
1		id 15	. 2 |- (-. ph -> -. ph)
2	1	pm2.21d 123	1 |- (-. ph -> (ph -> ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24 127  pm2.18 129  notnot2 130  simplim 182  simplimOLD 183  pm2.5OLD 185  peirceOLD 214  pm2.68 348  dfor2OLD 350  orel2 471  pm2.42 544  pm5.18OLD 984  mttOLD 1020  mt2biOLD 1021  pm4.82 1050  pm5.71 1061  dedlem0b 1081  dedlemb 1083  meredith 1475  meredithOLD 1476  3ornot23 1553  pm2.43bgbi 1574  hbim 1643  ax46to6 1655  ax467to6 1661  ax467to7 1662  19.33b 1729  hbimd 1749  sbi2 1879  ax11indi 2022  mo 2053  mo2 2060  exmo 2077  2mo 2110  elab3gf 2650  moeq3 2677  opthpr 3343  dvdemo1 3683  reusv2lem2 3968  reusv6OLD 3977  dfwe2 4007  ordunisuc2 4065  fimax 5846  xrub 7629  hbimtg 14514  tbw-bijust 14865  tbw-negdf 14866  merco2 14903  meran1 14935  imsym1 14942  cbcpcp 15243  fimaxOLD 16570  pm10.53 17137  pm11.63 17176  ax4567 17183  ax4567to4 17184  ax4567to6 17186  ax4567to7 17187  notnot2ALT 17308  notnot2ALTVD 17561

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain