Theorem orel1 212

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 197	. . 3 |- ((ph \/ ps) <-> (-. ph -> ps))
2	1	biimp 133	. 2 |- ((ph \/ ps) -> (-. ph -> ps))
3	2	com12 13	1 |- (-. ph -> ((ph \/ ps) -> ps))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195

This theorem is referenced by:  orel2 213  prel12 1875  funun 2700  tfrlem13 2961

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

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org