Metamath Proof Explorer

Theorem jaao

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

Ref Expression
Hypotheses jaao.1 φ ψ χ
jaao.2 θ τ χ
Assertion jaao φ θ ψ τ χ


Step Hyp Ref Expression
1 jaao.1 φ ψ χ
2 jaao.2 θ τ χ
3 1 adantr φ θ ψ χ
4 2 adantl φ θ τ χ
5 3 4 jaod φ θ ψ τ χ