Metamath Proof Explorer

Theorem orimdi

Description: Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013)

Ref Expression
Assertion orimdi ⊢ φ ∨ ψ → χ ↔ φ ∨ ψ → φ ∨ χ

Proof

Step Hyp Ref Expression
1 imdi ⊢ ¬ φ → ψ → χ ↔ ¬ φ → ψ → ¬ φ → χ
2 df-or ⊢ φ ∨ ψ → χ ↔ ¬ φ → ψ → χ
3 df-or ⊢ φ ∨ ψ ↔ ¬ φ → ψ
4 df-or ⊢ φ ∨ χ ↔ ¬ φ → χ
5 3 4 imbi12i ⊢ φ ∨ ψ → φ ∨ χ ↔ ¬ φ → ψ → ¬ φ → χ
6 1 2 5 3bitr4i ⊢ φ ∨ ψ → χ ↔ φ ∨ ψ → φ ∨ χ