This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		pm3.2i.1	$⊢ φ$
2		pm3.2i.2	$⊢ ψ$
3		pm3.2	$⊢ φ \to (ψ \to (φ \land ψ))$
4	1 2 3	mp2	$⊢ (φ \land ψ)$