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

Metamath Proof Explorer

Theorem moani

Description: "At most one" is still true when a conjunct is added, inference form. (Contributed by NM, 9-Mar-1995)

		Ref	Expression
	Hypothesis	moani.1	$⊢ \exists^{*} x φ$
	Assertion	moani	$⊢ \exists^{*} x (ψ \land φ)$

Step	Hyp	Ref	Expression
1		moani.1	$⊢ \exists^{*} x φ$
2		moan	$⊢ \exists^{} x φ \to \exists^{} x (ψ \land φ)$
3	1 2	ax-mp	$⊢ \exists^{*} x (ψ \land φ)$