Theorem jcai

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

	Ref	Expression
Hypotheses	jcai.1	|- ( ph -> ps )
	jcai.2	|- ( ph -> ( ps -> ch ) )
Assertion	jcai	|- ( ph -> ( ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		jcai.1	|- ( ph -> ps )
2		jcai.2	|- ( ph -> ( ps -> ch ) )
3	1 2	mpd	|- ( ph -> ch )
4	1 3	jca	|- ( ph -> ( ps /\ ch ) )