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 ⊢ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) )