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	|- (-. ph -> (ph -> ps))

Proof of Theorem pm2.21

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

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  2829  elab3gf  2991  moeq3  3014  pwadjoin  4120  dff3  5421