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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24 79  pm2.18 81  peirce 82  nega 84  pm2.5 100  pm3.26im 139  dfor2 229  pm2.42 343  pm5.18 659  mtt 711  mt2bi 712  pm4.82 738  pm5.71 747  dedlem0b 760  dedlemb 762  meredith 922  hbim 1005  ax46to6 1017  ax467to6 1023  ax467to7 1024  hbimd 1108  sbi2 1231  ax11indi 1365  mo 1391  mo2 1398  exmo 1414  2mo 1445  moeq3 1917  opthpr 2481  dvdemo1 2770  ordunisuc2 3110  xrub 6035

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

Copyright terms: Public domain