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 660  mtt 712  mt2bi 713  pm4.82 739  pm5.71 748  dedlem0b 761  dedlemb 763  meredith 924  hbim 1007  ax46to6 1019  ax467to6 1025  ax467to7 1026  hbimd 1110  sbi2 1233  ax11indi 1367  mo 1393  mo2 1400  exmo 1416  2mo 1447  moeq3 1921  opthpr 2485  dvdemo1 2775  ordunisuc2 3115  xrub 6080

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

Copyright terms: Public domain