Theorem 3pm3.2i

Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995)

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

Proof

Step	Hyp	Ref	Expression
1		3pm3.2i.1	|- ph
2		3pm3.2i.2	|- ps
3		3pm3.2i.3	|- ch
4	1 2	pm3.2i	|- ( ph /\ ps )
5		df-3an	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
6	4 3 5	mpbir2an	|- ( ph /\ ps /\ ch )