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

Theorem eximi 1751
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 1750 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1714 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  2eximi  1752  eximii  1753  exa1  1755  exan  1774  exsimpl  1782  exsimpr  1783  19.29r2  1791  19.29x  1792  19.35  1793  19.40-2  1802  exlimiv  1844  speimfwALT  1863  sbimi  1872  19.12  2148  ax13lem2  2282  axc9lem2OLD  2283  exdistrf  2320  equs45f  2337  mo2v  2464  2eu2ex  2533  reximi2  2992  cgsexg  3210  gencbvex  3222  vtocl3  3234  eqvinc  3299  axrep2  4695  bm1.3ii  4706  ax6vsep  4707  axnulOLD  4711  copsexg  4876  dminss  5452  imainss  5453  elsnxpOLD  5581  iotaex  5771  fv3  6101  ssimaex  6158  dffv2  6166  exfo  6270  oprabid  6554  zfrep6  7004  frxp  7151  suppimacnvss  7169  tz7.48-1  7402  enssdom  7843  fineqvlem  8036  infcntss  8096  infeq5  8394  omex  8400  rankuni  8586  scott0  8609  acni3  8730  acnnum  8735  dfac3  8804  dfac9  8818  kmlem1  8832  cflm  8932  cfcof  8956  axdc4lem  9137  axcclem  9139  ac6c4  9163  ac6s  9166  ac6s2  9168  axdclem2  9202  brdom3  9208  brdom5  9209  brdom4  9210  nqpr  9692  ltexprlem4  9717  reclem2pr  9726  hash1to3  13078  trclublem  13528  drsdirfi  16707  2ndcsb  21004  fbssint  21394  isfil2  21412  alexsubALTlem3  21605  lpbl  22059  metustfbas  22113  3v3e3cycl2  25958  ex-natded9.26-2  26435  eqvincg  28504  19.9d2rf  28508  rexunirn  28521  f1ocnt  28752  fmcncfil  29111  esumiun  29289  0elsiga  29310  ddemeas  29432  bnj168  29858  bnj593  29875  bnj607  30046  bnj600  30049  bnj916  30063  fundmpss  30716  exisym1  31399  bj-exlime  31602  bj-nalnaleximiOLD  31604  bj-sbex  31621  bj-ssbequ2  31638  bj-equs45fv  31748  bj-axrep2  31790  bj-eumo0  31831  bj-snsetex  31947  bj-snglss  31954  bj-snglex  31957  bj-restn0  32027  bj-toprntopon  32047  bj-ccinftydisj  32080  mptsnunlem  32164  spsbce-2  37405  iotaexeu  37444  iotasbc  37445  relopabVD  37962  ax6e2ndeqVD  37970  2uasbanhVD  37972  ax6e2ndeqALT  37992  fnchoice  38014  rfcnnnub  38021  stoweidlem35  38732  stoweidlem57  38754  n0rex  40115
  Copyright terms: Public domain W3C validator