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

Metamath Proof Explorer

Theorem orim12da

Description: Deduce a disjunction from another one. Variation on orim12d . (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses orim12da.1 ⊢ φ ∧ ψ → θ
orim12da.2 ⊢ φ ∧ χ → τ
orim12da.3 ⊢ φ → ψ ∨ χ
Assertion orim12da ⊢ φ → θ ∨ τ

Proof

Step Hyp Ref Expression
1 orim12da.1 ⊢ φ ∧ ψ → θ
2 orim12da.2 ⊢ φ ∧ χ → τ
3 orim12da.3 ⊢ φ → ψ ∨ χ
4 1 ex ⊢ φ → ψ → θ
5 2 ex ⊢ φ → χ → τ
6 4 5 orim12d ⊢ φ → ψ ∨ χ → θ ∨ τ
7 3 6 mpd ⊢ φ → θ ∨ τ