Theorem orim12da

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

Hypotheses
orim12da.1
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
orim12da.2
\( \vdash \varphi \wedge \chi \rightarrow \tau \)
orim12da.3
\( \vdash \varphi \rightarrow \psi \vee \chi \)
Conclusion
\( \vdash \varphi \rightarrow \theta \vee \tau \)
Proof
l0
orim12da.3
\( \vdash \varphi \rightarrow \psi \vee \chi \)
orim12da.1
l2
ex _
orim12da.2
ex _
orim12d l2 _
\( \vdash \varphi \rightarrow \psi \vee \chi \rightarrow \theta \vee \tau \)
mpd l0 _