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	$$⊢\phi$$
	pm3.2i.2	$$⊢\psi$$
Assertion	pm3.2i	$$⊢\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm3.2i.1	$$⊢\phi$$
2		pm3.2i.2	$$⊢\psi$$
3		pm3.2	$$⊢\phi \to \left(\psi \to \left(\phi \wedge \psi \right)\right)$$
4	1 2 3	mp2	$$⊢\left(\phi \wedge \psi \right)$$