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

Metamath Proof Explorer

Theorem simpli

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994)

		Ref	Expression
	Hypothesis	simpli.1	$⊢ (φ \land ψ)$
	Assertion	simpli	$⊢ φ$

Step	Hyp	Ref	Expression
1		simpli.1	$⊢ (φ \land ψ)$
2		simpl	$⊢ (φ \land ψ) \to φ$
3	1 2	ax-mp	$⊢ φ$