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

Theorem eximi 1661
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 1659 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1625 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-ex 1618
This theorem is referenced by:  2eximi  1662  eximii  1663  exa1  1666  exsimpl  1682  exsimpr  1683  19.29r2  1690  19.29x  1691  19.35  1692  19.40-2  1702  exlimiv  1727  speimfwOLD  1741  sbimi  1750  19.12  1955  axc9lem2  2044  exdistrf  2079  equs45f  2093  mo2v  2291  mo2vOLD  2292  mo2vOLDOLD  2293  2eu2ex  2365  reximi2  2921  cgsexg  3139  gencbvex  3150  vtocl3  3160  eqvinc  3223  axrep2  4552  bm1.3ii  4563  ax6vsep  4564  axnul  4567  copsexg  4722  dminss  5405  imainss  5406  iotaex  5551  fv3  5861  ssimaex  5913  dffv2  5921  exfo  6025  oprabid  6297  zfrep6  6741  frxp  6883  suppimacnvss  6901  tz7.48-1  7100  enssdom  7533  fineqvlem  7727  infcntss  7786  infeq5  8045  omex  8051  rankuni  8272  scott0  8295  acni3  8419  acnnum  8424  dfac3  8493  dfac9  8507  kmlem1  8521  cflm  8621  cfcof  8645  axdc4lem  8826  axcclem  8828  ac6c4  8852  ac6s  8855  ac6s2  8857  axdclem2  8891  brdom3  8897  brdom5  8898  brdom4  8899  nqpr  9381  ltexprlem4  9406  reclem2pr  9415  hash1to3  12517  trclublem  12916  drsdirfi  15769  2ndcsb  20119  fbssint  20508  isfil2  20526  alexsubALTlem3  20718  lpbl  21175  metustfbasOLD  21237  metustfbas  21238  3v3e3cycl2  24869  ex-natded9.26-2  25346  eqvincg  27575  19.9d2rf  27578  rexunirn  27591  elsnxp  27687  fmcncfil  28151  esumiun  28326  0elsiga  28347  ddemeas  28448  fundmpss  29440  exisym1  30120  spsbce-2  31530  iotaexeu  31569  iotasbc  31570  fnchoice  31647  rfcnnnub  31654  stoweidlem35  32059  stoweidlem57  32081  relopabVD  34121  ax6e2ndeqVD  34129  2uasbanhVD  34131  ax6e2ndeqALT  34151  bnj168  34205  bnj593  34222  bnj607  34394  bnj600  34397  bnj916  34411  bj-exlime  34640  bj-nalnaleximiOLD  34642  bj-exaleximi  34644  bj-equs45fv  34751  bj-axrep2  34795  bj-eumo0  34834  bj-snsetex  34941  bj-snglss  34948  bj-snglex  34951  bj-ccinftydisj  35035
  Copyright terms: Public domain W3C validator