Theorem jaao

Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)

Hypotheses
jaao.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
jaao.2
\( \vdash \theta \rightarrow \tau \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow \psi \vee \tau \rightarrow \chi \)
Proof
jaao.1
l1
adantr _
jaao.2
adantl _
jaod l1 _