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

Theorem eximi 1760
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 1759 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1722 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  2eximi  1761  eximii  1762  exa1  1763  exan  1786  exsimpl  1793  exsimpr  1794  19.29r2  1801  19.29x  1802  19.35  1803  19.40-2  1812  exlimiv  1856  speimfwALT  1875  sbimi  1884  19.12  2162  ax13lem2  2294  exdistrf  2331  equs45f  2348  mo2v  2475  2eu2ex  2544  reximi2  3007  cgsexg  3233  gencbvex  3245  vtocl3  3257  eqvinc  3324  n0rex  3927  axrep2  4764  bm1.3ii  4775  ax6vsep  4776  copsexg  4946  relopabi  5234  dminss  5535  imainss  5536  elsnxpOLD  5666  iotaex  5856  fv3  6193  ssimaex  6250  dffv2  6258  exfo  6363  oprabid  6662  zfrep6  7119  frxp  7272  suppimacnvss  7290  tz7.48-1  7523  enssdom  7965  fineqvlem  8159  infcntss  8219  infeq5  8519  omex  8525  rankuni  8711  scott0  8734  acni3  8855  acnnum  8860  dfac3  8929  dfac9  8943  kmlem1  8957  cflm  9057  cfcof  9081  axdc4lem  9262  axcclem  9264  ac6c4  9288  ac6s  9291  ac6s2  9293  axdclem2  9327  brdom3  9335  brdom5  9336  brdom4  9337  nqpr  9821  ltexprlem4  9846  reclem2pr  9855  hash1to3  13256  trclublem  13715  drsdirfi  16919  toprntopon  20710  2ndcsb  21233  fbssint  21623  isfil2  21641  alexsubALTlem3  21834  lpbl  22289  metustfbas  22343  ex-natded9.26-2  27247  eqvincg  29284  19.9d2rf  29289  rexunirn  29303  f1ocnt  29533  fsumiunle  29549  fmcncfil  29951  esumiun  30130  0elsiga  30151  ddemeas  30273  bnj168  30772  bnj593  30789  bnj607  30960  bnj600  30963  bnj916  30977  fundmpss  31640  exisym1  32398  bj-exlime  32584  bj-sbex  32601  bj-ssbequ2  32618  bj-equs45fv  32727  bj-axrep2  32764  bj-eumo0  32805  bj-snsetex  32926  bj-snglss  32933  bj-snglex  32936  bj-restn0  33018  bj-ccinftydisj  33071  mptsnunlem  33156  spsbce-2  38400  iotaexeu  38439  iotasbc  38440  relopabVD  38957  ax6e2ndeqVD  38965  2uasbanhVD  38967  ax6e2ndeqALT  38987  fnchoice  39008  rfcnnnub  39015  stoweidlem35  40015  stoweidlem57  40037
  Copyright terms: Public domain W3C validator