MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moani Structured version   Visualization version   GIF version

Theorem moani 2545
Description: "At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
Hypothesis
Ref Expression
moani.1 ∃*𝑥𝜑
Assertion
Ref Expression
moani ∃*𝑥(𝜓𝜑)

Proof of Theorem moani
StepHypRef Expression
1 moani.1 . 2 ∃*𝑥𝜑
2 moan 2544 . 2 (∃*𝑥𝜑 → ∃*𝑥(𝜓𝜑))
31, 2ax-mp 5 1 ∃*𝑥(𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 394  ∃*wmo 2530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-mo 2532
This theorem is referenced by:  euxfr2w  3717  euxfr2  3719  rmoeq  3735  reuxfrd  3745  fvopab6  7032  mpofun  7536  1stconst  8090  2ndconst  8091  pwfir  9180  iunmapdisj  10022  axaddf  11144  axmulf  11145  joinval  18336  meetval  18350  reuxfrdf  31996
  Copyright terms: Public domain W3C validator