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

Metamath Proof Explorer

Theorem jcai

Description: Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993)

Ref Expression
Hypotheses jcai.1 ⊢ φ → ψ
jcai.2 ⊢ φ → ψ → χ
Assertion jcai ⊢ φ → ψ ∧ χ

Proof

Step Hyp Ref Expression
1 jcai.1 ⊢ φ → ψ
2 jcai.2 ⊢ φ → ψ → χ
3 1 2 mpd ⊢ φ → χ
4 1 3 jca ⊢ φ → ψ ∧ χ