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	⊢ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) )