This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orbi12d

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypotheses bi12d.1 ⊢ φ → ψ ↔ χ
bi12d.2 ⊢ φ → θ ↔ τ
Assertion orbi12d ⊢ φ → ψ ∨ θ ↔ χ ∨ τ

Proof

Step Hyp Ref Expression
1 bi12d.1 ⊢ φ → ψ ↔ χ
2 bi12d.2 ⊢ φ → θ ↔ τ
3 1 orbi1d ⊢ φ → ψ ∨ θ ↔ χ ∨ θ
4 2 orbi2d ⊢ φ → χ ∨ θ ↔ χ ∨ τ
5 3 4 bitrd ⊢ φ → ψ ∨ θ ↔ χ ∨ τ