Metamath Proof Explorer

Theorem pm4.78

Description: Implication distributes over disjunction. Theorem *4.78 of WhiteheadRussell p. 121. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 19-Nov-2012)

Ref Expression
Assertion pm4.78 ⊢ φ → ψ ∨ φ → χ ↔ φ → ψ ∨ χ

Proof

Step Hyp Ref Expression
1 orordi ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ
2 imor ⊢ φ → ψ ∨ χ ↔ ¬ φ ∨ ψ ∨ χ
3 imor ⊢ φ → ψ ↔ ¬ φ ∨ ψ
4 imor ⊢ φ → χ ↔ ¬ φ ∨ χ
5 3 4 orbi12i ⊢ φ → ψ ∨ φ → χ ↔ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ
6 1 2 5 3bitr4ri ⊢ φ → ψ ∨ φ → χ ↔ φ → ψ ∨ χ