Metamath Proof Explorer

Theorem ja

Description: Inference joining the antecedents of two premises. For partial converses, see jarri and jarli . (Contributed by NM, 24-Jan-1993) (Proof shortened by Mel L. O'Cat, 19-Feb-2008)

Ref Expression
Hypotheses ja.1 ¬ φ χ
ja.2 ψ χ
Assertion ja φ ψ χ


Step Hyp Ref Expression
1 ja.1 ¬ φ χ
2 ja.2 ψ χ
3 2 imim2i φ ψ φ χ
4 3 1 pm2.61d1 φ ψ χ