This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ ∧ θ → ψ ∨ τ → χ

Proof

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