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

Theorem moani 2551
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 2550 . 2 (∃*𝑥𝜑 → ∃*𝑥(𝜓𝜑))
31, 2ax-mp 5 1 ∃*𝑥(𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wa 395  ∃*wmo 2536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-mo 2538
This theorem is referenced by:  euxfr2w  3729  euxfr2  3731  rmoeq  3747  reuxfrd  3757  fvopab6  7050  mpofun  7557  1stconst  8124  2ndconst  8125  pwfir  9353  iunmapdisj  10061  axaddf  11183  axmulf  11184  joinval  18435  meetval  18449  reuxfrdf  32519
  Copyright terms: Public domain W3C validator