Theorem 3pm3.2i

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

	Ref	Expression
Hypotheses	3pm3.2i.1	⊢ 𝜑
	3pm3.2i.2	⊢ 𝜓
	3pm3.2i.3	⊢ 𝜒
Assertion	3pm3.2i	⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		3pm3.2i.1	⊢ 𝜑
2		3pm3.2i.2	⊢ 𝜓
3		3pm3.2i.3	⊢ 𝜒
4	1 2	pm3.2i	⊢ ( 𝜑 ∧ 𝜓 )
5		df-3an	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
6	4 3 5	mpbir2an	⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 )