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

Theorem eximi 1701
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 1700 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1665 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  2eximi  1702  eximii  1703  exa1  1705  exsimpl  1723  exsimpr  1724  19.29r2  1732  19.29x  1733  19.35  1734  19.40-2  1743  exlimiv  1770  speimfwOLD  1787  sbimi  1796  19.12  2010  axc9lem2  2105  axc9lem2OLD  2106  exdistrf  2141  equs45f  2155  mo2v  2283  2eu2ex  2352  reximi2  2831  cgsexg  3056  gencbvex  3067  vtocl3  3078  eqvinc  3141  axrep2  4481  bm1.3ii  4492  ax6vsep  4493  axnulOLD  4497  copsexg  4649  dminss  5212  imainss  5213  elsnxp  5340  iotaex  5525  fv3  5838  ssimaex  5890  dffv2  5898  exfo  5999  oprabid  6276  zfrep6  6719  frxp  6861  suppimacnvss  6879  tz7.48-1  7115  enssdom  7548  fineqvlem  7739  infcntss  7798  infeq5  8095  omex  8101  rankuni  8286  scott0  8309  acni3  8429  acnnum  8434  dfac3  8503  dfac9  8517  kmlem1  8531  cflm  8631  cfcof  8655  axdc4lem  8836  axcclem  8838  ac6c4  8862  ac6s  8865  ac6s2  8867  axdclem2  8901  brdom3  8907  brdom5  8908  brdom4  8909  nqpr  9390  ltexprlem4  9415  reclem2pr  9424  hash1to3  12596  trclublem  13003  drsdirfi  16126  2ndcsb  20406  fbssint  20795  isfil2  20813  alexsubALTlem3  21006  lpbl  21460  metustfbas  21514  3v3e3cycl2  25334  ex-natded9.26-2  25812  eqvincg  28050  19.9d2rf  28054  rexunirn  28069  f1ocnt  28326  fmcncfil  28689  esumiun  28867  0elsiga  28888  ddemeas  29011  bnj168  29490  bnj593  29507  bnj607  29679  bnj600  29682  bnj916  29696  fundmpss  30358  exisym1  31033  bj-exlime  31164  bj-nalnaleximiOLD  31166  bj-equs45fv  31271  bj-axrep2  31315  bj-eumo0  31354  bj-snsetex  31468  bj-snglss  31475  bj-snglex  31478  bj-ccinftydisj  31562  mptsnunlem  31647  spsbce-2  36643  iotaexeu  36682  iotasbc  36683  relopabVD  37214  ax6e2ndeqVD  37222  2uasbanhVD  37224  ax6e2ndeqALT  37244  fnchoice  37266  rfcnnnub  37273  stoweidlem35  37779  stoweidlem57  37801
  Copyright terms: Public domain W3C validator