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

Theorem eximi 1625
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 1623 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1593 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  2eximi  1626  eximii  1627  exsimpl  1644  exsimpr  1645  19.29r2  1652  19.29x  1653  19.35  1654  19.40-2  1664  exlimiv  1688  speimfw  1697  sbimi  1706  19.12  1875  axc9lem2  1988  exdistrf  2025  equs45f  2041  mo2v  2259  mo2vOLD  2260  eumo0OLD  2289  eupickbOLD  2343  2eu2ex  2353  reximi2  2817  cgsexg  3000  gencbvex  3011  vtocl3  3021  eqvinc  3081  axrep2  4400  bm1.3ii  4411  ax6vsep  4412  axnul  4415  copsexg  4571  dminss  5246  imainss  5247  iotaex  5393  fv3  5698  ssimaex  5751  dffv2  5759  exfo  5856  oprabid  6110  zfrep6  6540  frxp  6677  suppimacnvss  6695  tz7.48-1  6890  enssdom  7326  fineqvlem  7519  infcntss  7577  infeq5  7835  omex  7841  rankuni  8062  scott0  8085  acni3  8209  acnnum  8214  dfac3  8283  dfac9  8297  kmlem1  8311  cflm  8411  cfcof  8435  axdc4lem  8616  axcclem  8618  ac6c4  8642  ac6s  8645  ac6s2  8647  axdclem2  8681  brdom3  8687  brdom5  8688  brdom4  8689  axpowndlem2  8754  axpowndlem2OLD  8755  nqpr  9175  ltexprlem4  9200  reclem2pr  9209  drsdirfi  15100  2ndcsb  19028  fbssint  19386  isfil2  19404  alexsubALTlem3  19596  lpbl  20053  metustfbasOLD  20115  metustfbas  20116  3v3e3cycl2  23501  ex-natded9.26-2  23578  eqvincg  25810  19.9d2rf  25813  rexunirn  25826  ceqsexv2d  25833  cnvoprab  25974  fmcncfil  26313  0elsiga  26509  ddemeas  26604  fundmpss  27528  exisym1  28222  heiborlem3  28665  spsbce-2  29586  iotaexeu  29625  iotasbc  29626  fnchoice  29704  rfcnnnub  29711  stoweidlem35  29783  stoweidlem57  29805  hash1to3  30188  relopabVD  31524  ax6e2ndeqVD  31532  2uasbanhVD  31534  ax6e2ndeqALT  31554  bnj168  31608  bnj593  31624  bnj607  31796  bnj600  31799  bnj916  31813  bj-exa1  32020  bj-nalnaleximiOLD  32044  bj-exaleximi  32046  bj-equs45fv  32123  bj-axrep2  32167  bj-eumo0  32205  bj-snsetex  32303  bj-snglss  32310  bj-snglex  32313  bj-ccinftydisj  32383
  Copyright terms: Public domain W3C validator