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

Metamath Proof Explorer

Theorem moan

Description: "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995)

		Ref	Expression
	Assertion	moan	$⊢ \exists^{} x φ \to \exists^{} x (ψ \land φ)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (ψ \land φ) \to φ$
2	1	moimi	$⊢ \exists^{} x φ \to \exists^{} x (ψ \land φ)$