Metamath Proof Explorer

Theorem jaoa

Description: Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008)

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


Step Hyp Ref Expression
1 jaao.1 φ ψ χ
2 jaao.2 θ τ χ
3 1 adantrd φ ψ τ χ
4 2 adantld θ ψ τ χ
5 3 4 jaoi φ θ ψ τ χ