Theorem pm2.21 71

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 3	. 2 |- (-. ph -> (-. ps -> -. ph))
2	1	a3d 70	1 |- (-. ph -> (ph -> ps))

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  pm2.24 72  pm2.18 75  peirce 76  nega 78  pm3.26im 120  dfor2 199  pm5.18 497  mtt 534  mt2bi 535  nbn 542  dedlem0b 568  dedlemb 570  meredith 644  hbim 702  hbimd 787  sbi2 885  mo 1020  mo2 1026  exmo 1042  moeq3 1432

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

metamath.org