Theorem imor 204

Description: Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120.

Assertion

Ref	Expression
imor	⊢ ((φ → ψ) ↔ (¬ φ ∨ ψ))

Proof of Theorem imor

Step	Hyp	Ref	Expression
1		pm4.13 142	. . 3 ⊢ (φ ↔ ¬ ¬ φ)
2	1	imbi1i 161	. 2 ⊢ ((φ → ψ) ↔ (¬ ¬ φ → ψ))
3		df-or 197	. 2 ⊢ ((¬ φ ∨ ψ) ↔ (¬ ¬ φ → ψ))
4	2, 3	bitr4 154	1 ⊢ ((φ → ψ) ↔ (¬ φ ∨ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195

This theorem is referenced by:  anor 252  pm2.85 439  jcab 454  19.30 764  iununi 2037  kmlem4 3583  chrelat2 5758

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