Metamath Proof Explorer

Theorem jaoi

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994)

Ref Expression
Hypotheses jaoi.1 φ ψ
jaoi.2 χ ψ
Assertion jaoi φ χ ψ


Step Hyp Ref Expression
1 jaoi.1 φ ψ
2 jaoi.2 χ ψ
3 pm2.53 φ χ ¬ φ χ
4 3 2 syl6 φ χ ¬ φ ψ
5 4 1 pm2.61d2 φ χ ψ