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

Metamath Proof Explorer

Theorem orim12i

Description: Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994) (Proof shortened by Wolf Lammen, 25-Jul-2012)

Ref Expression
Hypotheses orim12i.1 ⊢ φ → ψ
orim12i.2 ⊢ χ → θ
Assertion orim12i ⊢ φ ∨ χ → ψ ∨ θ

Proof

Step Hyp Ref Expression
1 orim12i.1 ⊢ φ → ψ
2 orim12i.2 ⊢ χ → θ
3 1 orcd ⊢ φ → ψ ∨ θ
4 2 olcd ⊢ χ → ψ ∨ θ
5 3 4 jaoi ⊢ φ ∨ χ → ψ ∨ θ