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

Theorem eximi 1585
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-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 1584 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1557 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  2eximi  1586  eximii  1587  exsimpl  1602  19.29r2  1608  19.29x  1609  19.40  1619  19.40-2  1620  exlimiv  1644  speimfw  1655  spsbe  1663  sbimi  1664  exlimivOLD  1711  19.12  1869  19.12OLD  1870  equs4OLD  1998  ax12olem2  2006  exdistrf  2062  exdistrfOLD  2063  equs45f  2084  sbequi  2136  sbequiOLD  2137  eumo0  2304  euan  2337  eupickb  2345  2eu2ex  2354  rexex  2757  reximi2  2804  cgsexg  2979  gencbvex  2990  vtocl3  3000  eqvinc  3055  axrep2  4314  bm1.3ii  4325  ax9vsep  4326  axnul  4329  imassrn  5208  dminss  5278  imainss  5279  iotaex  5427  fv3  5736  ssimaex  5780  dffv2  5788  exfo  5879  zfrep6  5960  oprabid  6097  frxp  6448  tz7.48-1  6692  enssdom  7124  fineqvlem  7315  infcntss  7372  infeq5  7582  omex  7588  rankuni  7779  scott0  7800  acni3  7918  finacn  7921  acnnum  7923  dfac3  7992  dfac4  7993  dfac9  8006  kmlem1  8020  kmlem2  8021  cflm  8120  cfcof  8144  axdc4lem  8325  axcclem  8327  ac6c4  8351  ac6c5  8352  ac6s  8354  ac6s2  8356  ac6s3  8357  ac6s5  8361  axdclem2  8390  brdom3  8396  brdom5  8397  brdom4  8398  axpowndlem2  8463  nqpr  8881  ltexprlem4  8906  reclem2pr  8915  drsdirfi  14385  2ndcsb  17502  fbssint  17860  isfil2  17878  alexsubALTlem3  18070  lpbl  18523  metustfbasOLD  18585  metustfbas  18586  3v3e3cycl2  21641  ex-natded9.26-2  21718  eqvincg  23951  19.9d2rf  23958  rexunirn  23968  ceqsexv2d  23975  fmcncfil  24307  0elsiga  24487  fundmpss  25378  exisym1  26139  heiborlem3  26476  exan3  26655  spsbce-2  27511  iotaexeu  27550  iotasbc  27551  fnchoice  27631  rfcnnnub  27638  stoweidlem35  27715  stoweidlem57  27737  relopabVD  28914  a9e2ndeqVD  28922  2uasbanhVD  28924  a9e2ndeqALT  28944  bnj168  28998  bnj593  29014  bnj607  29188  bnj600  29191  bnj916  29205  19.12vAUX7  29355  exdistrfNEW7  29406  equs4NEW7  29434  sbequiNEW7  29480  equs45fNEW7  29522  19.12OLD7  29587
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator