Theorem pm3.2i

Description: Infer conjunction of premises. Inference associated with pm3.2 . Its associated deduction is jca (and the double deduction is jcad ). (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypotheses	pm3.2i.1	|- ph
	pm3.2i.2	|- ps
Assertion	pm3.2i	|- ( ph /\ ps )

Proof

Step	Hyp	Ref	Expression
1		pm3.2i.1	|- ph
2		pm3.2i.2	|- ps
3		pm3.2	|- ( ph -> ( ps -> ( ph /\ ps ) ) )
4	1 2 3	mp2	|- ( ph /\ ps )