Theorem 3orim123da

Disjoin antecedents and consequents of three premises. (Contributed by Thierry Arnoux, 13-Jul-2026.)

Hypotheses
3orim123da.1
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \eta \)
3orim123da.2
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
3orim123da.3
\( \vdash \varphi \wedge \theta \rightarrow \tau \)
3orim123da.4
\( \vdash \varphi \wedge \eta \rightarrow \zeta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \vee \tau \vee \zeta \)
Proof
l0
3orim123da.1
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \eta \)
3orim123da.2
l2
ex _
3orim123da.3
l4
ex _
3orim123da.4
ex _
3orim123d l2 l4 _
\( \vdash \varphi \rightarrow \psi \vee \theta \vee \eta \rightarrow \chi \vee \tau \vee \zeta \)
mpd l0 _