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 ( ∃* 𝑥 ( 𝜑𝜓 ) → ∃* 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 orc ( 𝜑 → ( 𝜑𝜓 ) )
2 1 moimi ( ∃* 𝑥 ( 𝜑𝜓 ) → ∃* 𝑥 𝜑 )