Theorem orel1 212

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

Assertion

Ref	Expression
orel1	⊢ (¬ φ → ((φ ∨ ψ) → ψ))

Proof of Theorem orel1

Step	Hyp	Ref	Expression
1		df-or 197	. . 3 ⊢ ((φ ∨ ψ) ↔ (¬ φ → ψ))
2	1	biimp 133	. 2 ⊢ ((φ ∨ ψ) → (¬ φ → ψ))
3	2	com12 13	1 ⊢ (¬ φ → ((φ ∨ ψ) → ψ))

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