Theorem 3jaaoOLD

Obsolete version of 3jaao as of 16-Jun-2026. Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
3jaao.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3jaao.2
\( \vdash \theta \rightarrow \tau \rightarrow \chi \)
3jaao.3
\( \vdash \eta \rightarrow \zeta \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \theta \wedge \eta \rightarrow \psi \vee \tau \vee \zeta \rightarrow \chi \)
Proof
3jaao.1
l1
3ad2ant1 _
3jaao.2
l3
3ad2ant2 _
3jaao.3
3ad2ant3 _
3jaod l1 l3 _