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

Theorem eximi 1635
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 1633 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1603 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  2eximi  1636  eximii  1637  exsimpl  1654  exsimpr  1655  19.29r2  1662  19.29x  1663  19.35  1664  19.40-2  1674  exlimiv  1698  speimfwOLD  1708  sbimi  1717  19.12  1897  axc9lem2  2013  exdistrf  2048  equs45f  2064  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  eumo0OLD  2313  eupickbOLD  2367  2eu2ex  2377  reximi2  2931  cgsexg  3146  gencbvex  3157  vtocl3  3167  eqvinc  3230  axrep2  4560  bm1.3ii  4571  ax6vsep  4572  axnul  4575  copsexg  4732  dminss  5418  imainss  5419  iotaex  5566  fv3  5877  ssimaex  5930  dffv2  5938  exfo  6037  oprabid  6306  zfrep6  6749  frxp  6890  suppimacnvss  6908  tz7.48-1  7105  enssdom  7537  fineqvlem  7731  infcntss  7790  infeq5  8050  omex  8056  rankuni  8277  scott0  8300  acni3  8424  acnnum  8429  dfac3  8498  dfac9  8512  kmlem1  8526  cflm  8626  cfcof  8650  axdc4lem  8831  axcclem  8833  ac6c4  8857  ac6s  8860  ac6s2  8862  axdclem2  8896  brdom3  8902  brdom5  8903  brdom4  8904  axpowndlem2  8969  axpowndlem2OLD  8970  nqpr  9388  ltexprlem4  9413  reclem2pr  9422  hash1to3  12492  drsdirfi  15421  2ndcsb  19716  fbssint  20074  isfil2  20092  alexsubALTlem3  20284  lpbl  20741  metustfbasOLD  20803  metustfbas  20804  3v3e3cycl2  24340  ex-natded9.26-2  24818  eqvincg  27050  19.9d2rf  27053  rexunirn  27066  ceqsexv2d  27073  cnvoprab  27218  fmcncfil  27549  0elsiga  27754  ddemeas  27848  fundmpss  28773  exisym1  29466  heiborlem3  29912  spsbce-2  30864  iotaexeu  30903  iotasbc  30904  fnchoice  30982  rfcnnnub  30989  stoweidlem35  31335  stoweidlem57  31357  relopabVD  32781  ax6e2ndeqVD  32789  2uasbanhVD  32791  ax6e2ndeqALT  32811  bnj168  32865  bnj593  32881  bnj607  33053  bnj600  33056  bnj916  33070  bj-exa1  33287  bj-nalnaleximiOLD  33311  bj-exaleximi  33313  bj-equs45fv  33412  bj-axrep2  33456  bj-eumo0  33495  bj-snsetex  33602  bj-snglss  33609  bj-snglex  33612  bj-ccinftydisj  33688  trclubg  36795
  Copyright terms: Public domain W3C validator