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

Theorem eximi 1740
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 1739 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1702 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 1700  ax-4 1713
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  2eximi  1741  eximii  1742  exa1  1744  exsimpl  1764  exsimpr  1765  19.29r2  1773  19.29x  1774  19.35  1775  19.40-2  1784  exlimiv  1811  speimfwALT  1827  sbimi  1836  19.12  2082  ax13lem2  2187  axc9lem2OLD  2188  exdistrf  2225  equs45f  2242  mo2v  2369  2eu2ex  2438  reximi2  2897  cgsexg  3115  gencbvex  3127  vtocl3  3139  eqvinc  3204  axrep2  4599  bm1.3ii  4610  ax6vsep  4611  axnulOLD  4615  copsexg  4780  dminss  5356  imainss  5357  elsnxpOLD  5485  iotaex  5675  fv3  6005  ssimaex  6062  dffv2  6070  exfo  6174  oprabid  6458  zfrep6  6907  frxp  7054  suppimacnvss  7072  tz7.48-1  7305  enssdom  7746  fineqvlem  7939  infcntss  7999  infeq5  8297  omex  8303  rankuni  8489  scott0  8512  acni3  8633  acnnum  8638  dfac3  8707  dfac9  8721  kmlem1  8735  cflm  8835  cfcof  8859  axdc4lem  9040  axcclem  9042  ac6c4  9066  ac6s  9069  ac6s2  9071  axdclem2  9105  brdom3  9111  brdom5  9112  brdom4  9113  nqpr  9595  ltexprlem4  9620  reclem2pr  9629  hash1to3  12995  trclublem  13445  drsdirfi  16657  2ndcsb  20969  fbssint  21359  isfil2  21377  alexsubALTlem3  21570  lpbl  22024  metustfbas  22078  3v3e3cycl2  25934  ex-natded9.26-2  26411  eqvincg  28490  19.9d2rf  28494  rexunirn  28507  f1ocnt  28745  fmcncfil  29105  esumiun  29283  0elsiga  29304  ddemeas  29426  bnj168  29901  bnj593  29918  bnj607  30089  bnj600  30092  bnj916  30106  fundmpss  30756  exisym1  31431  bj-exlime  31634  bj-nalnaleximiOLD  31636  bj-sbex  31653  bj-ssbequ2  31670  bj-equs45fv  31780  bj-axrep2  31822  bj-eumo0  31863  bj-snsetex  31979  bj-snglss  31986  bj-snglex  31989  bj-restn0  32059  bj-toprntopon  32079  bj-ccinftydisj  32112  mptsnunlem  32196  spsbce-2  37503  iotaexeu  37542  iotasbc  37543  relopabVD  38060  ax6e2ndeqVD  38068  2uasbanhVD  38070  ax6e2ndeqALT  38090  fnchoice  38112  rfcnnnub  38119  stoweidlem35  38835  stoweidlem57  38857  n0rex  40222
  Copyright terms: Public domain W3C validator