Theorem pm2.21 92

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law.

Assertion

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

Proof of Theorem pm2.21

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 |- (-. ph -> (-. ps -> -. ph))
2	1	con4d 91	1 |- (-. ph -> (ph -> ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24 95  pm2.18 97  peirce 98  notnot2 100  pm2.5 115  simplim 154  dfor2 246  pm2.42 370  pm5.18 722  pm5.18OLD 723  mtt 780  mt2bi 781  pm4.82 811  pm5.71 820  dedlem0b 836  dedlemb 839  dedlembOLD 840  meredith 1200  meredithOLD 1201  hbim 1354  ax46to6 1366  ax467to6 1372  ax467to7 1373  19.33b 1444  hbimd 1468  sbi2 1603  ax11indi 1758  mo 1787  mo2 1795  exmo 1812  2mo 1851  elab3gf 2408  elab3gOLD 2410  moeq3 2432  opthpr 3156  dvdemo1 3520  eufromeq2 3829  eufromeq6 3833  dfwe2 3861  ordunisuc2 3926  xrub 7289  hbimtg 13873  tbw-bijust 14165  tbw-negdf 14166  merco2 14203  meran1 14235  imsym1 14242  cbcpcp 14504  fimax 15746  pm10.53 16313  pm11.63 16352  ax4567 16359  ax4567to4 16360  ax4567to6 16362  ax4567to7 16363

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

Copyright terms: Public domain