Theorem 3pm3.2i

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

	Ref	Expression
Hypotheses	3pm3.2i.1	$$⊢\phi$$
	3pm3.2i.2	$$⊢\psi$$
	3pm3.2i.3	$$⊢\chi$$
Assertion	3pm3.2i	$$⊢\left(\phi \wedge \psi \wedge \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		3pm3.2i.1	$$⊢\phi$$
2		3pm3.2i.2	$$⊢\psi$$
3		3pm3.2i.3	$$⊢\chi$$
4	1 2	pm3.2i	$$⊢\left(\phi \wedge \psi \right)$$
5		df-3an	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\wedge \chi \right)$$
6	4 3 5	mpbir2an	$$⊢\left(\phi \wedge \psi \wedge \chi \right)$$