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

Metamath Proof Explorer

Theorem jaoian

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005)

Ref Expression
Hypotheses jaoian.1 ⊢ φ ∧ ψ → χ
jaoian.2 ⊢ θ ∧ ψ → χ
Assertion jaoian ⊢ φ ∨ θ ∧ ψ → χ

Proof

Step Hyp Ref Expression
1 jaoian.1 ⊢ φ ∧ ψ → χ
2 jaoian.2 ⊢ θ ∧ ψ → χ
3 1 ex ⊢ φ → ψ → χ
4 2 ex ⊢ θ → ψ → χ
5 3 4 jaoi ⊢ φ ∨ θ → ψ → χ
6 5 imp ⊢ φ ∨ θ ∧ ψ → χ