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

Theorem moani 2548
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 2547 . 2 (∃*𝑥𝜑 → ∃*𝑥(𝜓𝜑))
31, 2ax-mp 5 1 ∃*𝑥(𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 397  ∃*wmo 2533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535
This theorem is referenced by:  euxfr2w  3717  euxfr2  3719  rmoeq  3735  reuxfrd  3745  fvopab6  7032  mpofun  7532  1stconst  8086  2ndconst  8087  pwfir  9176  iunmapdisj  10018  axaddf  11140  axmulf  11141  joinval  18330  meetval  18344  reuxfrdf  31731
  Copyright terms: Public domain W3C validator