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

Theorem moani 2552
Description: "At most one" is still true when a conjunct is added, inference form. (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 2551 . 2 (∃*𝑥𝜑 → ∃*𝑥(𝜓𝜑))
31, 2ax-mp 5 1 ∃*𝑥(𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 395  ∃*wmo 2537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-mo 2539
This theorem is referenced by:  euxfr2w  3725  euxfr2  3727  rmoeq  3743  reuxfrd  3753  fvopab6  7049  mpofun  7558  1stconst  8126  2ndconst  8127  pwfir  9356  iunmapdisj  10064  axaddf  11186  axmulf  11187  joinval  18423  meetval  18437  reuxfrdf  32511
  Copyright terms: Public domain W3C validator