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

Theorem eximi 1826
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 1825 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1789 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  2eximi  1827  eximii  1828  exa1  1829  exsimpl  1860  exsimpr  1861  19.29r2  1867  19.29x  1868  19.35  1869  19.40-2  1879  emptyex  1899  exlimiv  1922  speimfwALT  1958  spsbeOLD  2080  19.12  2337  ax13lem2  2385  exdistrf  2461  equs45f  2474  sbimiOLD  2508  sbimiALT  2570  dfmoeu  2611  moimi  2620  eu6  2652  2eu2ex  2721  reximi2  3241  cgsexg  3535  gencbvex  3547  eqvincg  3638  n0rex  4311  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  6863  oprabidw  7176  oprabid  7177  zfrep6  7645  frxp  7809  suppimacnvss  7829  tz7.48-1  8068  enssdom  8522  fineqvlem  8720  infcntss  8780  infeq5  9088  omex  9094  rankuni  9280  scott0  9303  acni3  9461  acnnum  9466  dfac3  9535  dfac9  9550  kmlem1  9564  cflm  9660  cfcof  9684  axdc4lem  9865  axcclem  9867  ac6c4  9891  ac6s  9894  ac6s2  9896  axdclem2  9930  brdom3  9938  brdom5  9939  brdom4  9940  nqpr  10424  ltexprlem4  10449  reclem2pr  10458  hash1to3  13837  trclublem  14343  fnpr2ob  16819  drsdirfi  17536  toprntopon  21461  2ndcsb  21985  fbssint  22374  isfil2  22392  alexsubALTlem3  22585  lpbl  23040  metustfbas  23094  ex-natded9.26-2  28126  19.9d2rf  30162  rexunirn  30183  f1ocnt  30451  fsumiunle  30472  fmcncfil  31073  esumiun  31252  0elsiga  31272  ddemeas  31394  bnj168  31899  bnj593  31915  bnj607  32087  bnj600  32090  bnj916  32104  lfuhgr3  32263  cusgredgex  32265  loop1cycl  32281  umgr2cycl  32285  fundmpss  32906  exisym1  33669  bj-sylge  33854  bj-19.12  33987  bj-equs45fv  34030  bj-snsetex  34172  bj-snglss  34179  bj-snglex  34182  bj-bm1.3ii  34251  bj-restn0  34275  bj-ccinftydisj  34387  mptsnunlem  34501  pibt2  34580  wl-cbvmotv  34635  wl-moae  34638  wl-nax6im  34640  iscard4  39778  spsbce-2  40590  iotaexeu  40627  iotasbc  40628  relopabVD  41112  ax6e2ndeqVD  41120  2uasbanhVD  41122  ax6e2ndeqALT  41142  fnchoice  41163  rfcnnnub  41170  stoweidlem35  42197  stoweidlem57  42219
  Copyright terms: Public domain W3C validator