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

Metamath Proof Explorer

Theorem moor

Description: "At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004)

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

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