Theorem jcai

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

	Ref	Expression
Hypotheses	jcai.1	$$⊢\phi \to \psi$$
	jcai.2	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	jcai	$$⊢\phi \to \left(\psi \wedge \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		jcai.1	$$⊢\phi \to \psi$$
2		jcai.2	$$⊢\phi \to \left(\psi \to \chi \right)$$
3	1 2	mpd	$$⊢\phi \to \chi$$
4	1 3	jca	$$⊢\phi \to \left(\psi \wedge \chi \right)$$