Theorem pm2.21 76

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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24 79  pm2.18 81  peirce 82  notnot2 84  pm2.5 99  pm3.26im 137  dfor2 227  pm2.42 341  pm5.18 663  mtt 717  mt2bi 718  pm4.82 744  pm5.71 753  dedlem0b 766  dedlemb 768  meredith 931  hbim 1043  ax46to6 1055  ax467to6 1061  ax467to7 1062  hbimd 1146  sbi2 1270  ax11indi 1406  mo 1432  mo2 1439  exmo 1455  2mo 1487  moeq3 1967  opthpr 2550  dvdemo1 2851  ordunisuc2 3198  xrub 6248  fimax 11837

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

Copyright terms: Public domain