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

Theorem eximi 1828
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
eximi.1 (𝜑𝜓)
Assertion
Ref Expression
eximi (∃𝑥𝜑 → ∃𝑥𝜓)

Proof of Theorem eximi
StepHypRef Expression
1 exim 1827 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1791 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 209  df-ex 1774
This theorem is referenced by:  2eximi  1829  eximii  1830  exa1  1831  exsimpl  1862  exsimpr  1863  19.29r2  1869  19.29x  1870  19.35  1871  19.40-2  1881  emptyex  1901  exlimiv  1924  speimfwALT  1960  spsbeOLD  2082  19.12  2339  ax13lem2  2387  exdistrf  2462  equs45f  2475  sbimiOLD  2509  sbimiALT  2571  dfmoeu  2612  moimi  2621  eu6  2653  2eu2ex  2722  reximi2  3242  cgsexg  3536  gencbvex  3548  eqvincg  3639  n0rex  4312  axrep2  5184  bm1.3ii  5197  ax6vsep  5198  copsexgw  5372  copsexg  5373  relopabi  5687  dminss  6003  imainss  6004  iotaex  6328  fv3  6681  ssimaex  6741  dffv2  6749  exfo  6864  oprabidw  7179  oprabid  7180  zfrep6  7648  frxp  7812  suppimacnvss  7832  tz7.48-1  8071  enssdom  8526  fineqvlem  8724  infcntss  8784  infeq5  9092  omex  9098  rankuni  9284  scott0  9307  acni3  9465  acnnum  9470  dfac3  9539  dfac9  9554  kmlem1  9568  cflm  9664  cfcof  9688  axdc4lem  9869  axcclem  9871  ac6c4  9895  ac6s  9898  ac6s2  9900  axdclem2  9934  brdom3  9942  brdom5  9943  brdom4  9944  nqpr  10428  ltexprlem4  10453  reclem2pr  10462  hash1to3  13841  trclublem  14347  fnpr2ob  16823  drsdirfi  17540  toprntopon  21525  2ndcsb  22049  fbssint  22438  isfil2  22456  alexsubALTlem3  22649  lpbl  23105  metustfbas  23159  ex-natded9.26-2  28191  19.9d2rf  30227  rexunirn  30248  f1ocnt  30517  fsumiunle  30538  fmcncfil  31162  esumiun  31341  0elsiga  31361  ddemeas  31483  bnj168  31988  bnj593  32004  bnj607  32176  bnj600  32179  bnj916  32193  lfuhgr3  32354  cusgredgex  32356  loop1cycl  32372  umgr2cycl  32376  fundmpss  32997  exisym1  33760  bj-sylge  33945  bj-19.12  34078  bj-equs45fv  34121  bj-snsetex  34263  bj-snglss  34270  bj-snglex  34273  bj-bm1.3ii  34344  bj-restn0  34368  bj-ccinftydisj  34482  mptsnunlem  34606  pibt2  34685  wl-cbvmotv  34740  wl-moae  34743  wl-nax6im  34745  iscard4  39885  spsbce-2  40698  iotaexeu  40735  iotasbc  40736  relopabVD  41220  ax6e2ndeqVD  41228  2uasbanhVD  41230  ax6e2ndeqALT  41250  fnchoice  41271  rfcnnnub  41278  stoweidlem35  42305  stoweidlem57  42327
  Copyright terms: Public domain W3C validator