Theorem orel1 271

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107.

Assertion

Ref	Expression
orel1	|- (-. ph -> ((ph \/ ps) -> ps))

Proof of Theorem orel1

Step	Hyp	Ref	Expression
1		df-or 241	. . 3 |- ((ph \/ ps) <-> (-. ph -> ps))
2	1	biimpi 168	. 2 |- ((ph \/ ps) -> (-. ph -> ps))
3	2	com12 14	1 |- (-. ph -> ((ph \/ ps) -> ps))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239

This theorem is referenced by:  orel2 272  pm2.25 273  pm2.53 274  ordi 656  euor2 1839  prel12 3155  xpcan 4348  funun 4462  tfrlem13 5131  3orel1 13805  3orel13 13816  dfon2lem4 13852  dfon2lem6 13854  soxp 13950

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

This theorem depends on definitions:  df-bi 164  df-or 241

Copyright terms: Public domain