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

Metamath Proof Explorer

Theorem jad

Description: Deduction form of ja . (Contributed by Scott Fenton, 13-Dec-2010) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Hypotheses jad.1 ⊢ φ → ¬ ψ → θ
jad.2 ⊢ φ → χ → θ
Assertion jad ⊢ φ → ψ → χ → θ

Proof

Step Hyp Ref Expression
1 jad.1 ⊢ φ → ¬ ψ → θ
2 jad.2 ⊢ φ → χ → θ
3 1 com12 ⊢ ¬ ψ → φ → θ
4 2 com12 ⊢ χ → φ → θ
5 3 4 ja ⊢ ψ → χ → φ → θ
6 5 com12 ⊢ φ → ψ → χ → θ