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