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	⊢ 𝜑
	pm3.2i.2	⊢ 𝜓
Assertion	pm3.2i	⊢ ( 𝜑 ∧ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		pm3.2i.1	⊢ 𝜑
2		pm3.2i.2	⊢ 𝜓
3		pm3.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
4	1 2 3	mp2	⊢ ( 𝜑 ∧ 𝜓 )