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

Theorem eximi 1626
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
eximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
eximi  |-  ( E. x ph  ->  E. x ps )

Proof of Theorem eximi
StepHypRef Expression
1 exim 1624 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1594 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  2eximi  1627  eximii  1628  exsimpl  1645  exsimpr  1646  19.29r2  1653  19.29x  1654  19.35  1655  19.40-2  1665  exlimiv  1689  speimfwOLD  1699  sbimi  1708  19.12  1888  axc9lem2  2000  exdistrf  2035  equs45f  2051  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  eumo0OLD  2300  eupickbOLD  2354  2eu2ex  2364  reximi2  2926  cgsexg  3109  gencbvex  3120  vtocl3  3130  eqvinc  3191  axrep2  4512  bm1.3ii  4523  ax6vsep  4524  axnul  4527  copsexg  4683  dminss  5358  imainss  5359  iotaex  5505  fv3  5811  ssimaex  5864  dffv2  5872  exfo  5969  oprabid  6223  zfrep6  6654  frxp  6791  suppimacnvss  6809  tz7.48-1  7007  enssdom  7443  fineqvlem  7637  infcntss  7695  infeq5  7953  omex  7959  rankuni  8180  scott0  8203  acni3  8327  acnnum  8332  dfac3  8401  dfac9  8415  kmlem1  8429  cflm  8529  cfcof  8553  axdc4lem  8734  axcclem  8736  ac6c4  8760  ac6s  8763  ac6s2  8765  axdclem2  8799  brdom3  8805  brdom5  8806  brdom4  8807  axpowndlem2  8872  axpowndlem2OLD  8873  nqpr  9293  ltexprlem4  9318  reclem2pr  9327  drsdirfi  15226  2ndcsb  19184  fbssint  19542  isfil2  19560  alexsubALTlem3  19752  lpbl  20209  metustfbasOLD  20271  metustfbas  20272  3v3e3cycl2  23701  ex-natded9.26-2  23778  eqvincg  26010  19.9d2rf  26013  rexunirn  26026  ceqsexv2d  26033  cnvoprab  26173  fmcncfil  26505  0elsiga  26701  ddemeas  26795  fundmpss  27720  exisym1  28413  heiborlem3  28859  spsbce-2  29780  iotaexeu  29819  iotasbc  29820  fnchoice  29898  rfcnnnub  29905  stoweidlem35  29977  stoweidlem57  29999  hash1to3  30382  relopabVD  31954  ax6e2ndeqVD  31962  2uasbanhVD  31964  ax6e2ndeqALT  31984  bnj168  32038  bnj593  32054  bnj607  32226  bnj600  32229  bnj916  32243  bj-exa1  32458  bj-nalnaleximiOLD  32482  bj-exaleximi  32484  bj-equs45fv  32583  bj-axrep2  32627  bj-eumo0  32666  bj-snsetex  32773  bj-snglss  32780  bj-snglex  32783  bj-ccinftydisj  32859
  Copyright terms: Public domain W3C validator