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

Theorem eximi 1626
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 1625 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1596 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-ex 1590
This theorem is referenced by:  2eximi  1627  eximii  1628  exsimpl  1644  exsimpr  1645  19.29r2  1652  19.29x  1653  19.40-2  1663  exlimiv  1687  speimfw  1696  sbimi  1705  19.12  1874  axc9lem2  1987  exdistrf  2024  equs45f  2040  mo2v  2260  eumo0OLD  2288  eupickbOLD  2341  2eu2ex  2351  reximi2  2812  cgsexg  2994  gencbvex  3005  vtocl3  3015  eqvinc  3075  axrep2  4393  bm1.3ii  4404  ax6vsep  4405  axnul  4408  dminss  5239  imainss  5240  iotaex  5386  fv3  5691  ssimaex  5744  dffv2  5752  exfo  5849  oprabid  6104  zfrep6  6534  frxp  6671  suppimacnvss  6689  tz7.48-1  6884  enssdom  7322  fineqvlem  7515  infcntss  7573  infeq5  7831  omex  7837  rankuni  8058  scott0  8081  acni3  8205  acnnum  8210  dfac3  8279  dfac9  8293  kmlem1  8307  cflm  8407  cfcof  8431  axdc4lem  8612  axcclem  8614  ac6c4  8638  ac6s  8641  ac6s2  8643  axdclem2  8677  brdom3  8683  brdom5  8684  brdom4  8685  axpowndlem2  8750  axpowndlem2OLD  8751  nqpr  9171  ltexprlem4  9196  reclem2pr  9205  drsdirfi  15091  2ndcsb  18895  fbssint  19253  isfil2  19271  alexsubALTlem3  19463  lpbl  19920  metustfbasOLD  19982  metustfbas  19983  3v3e3cycl2  23373  ex-natded9.26-2  23450  eqvincg  25682  19.9d2rf  25685  rexunirn  25699  ceqsexv2d  25706  cnvoprab  25847  fmcncfil  26215  0elsiga  26411  ddemeas  26506  fundmpss  27424  exisym1  28118  heiborlem3  28556  spsbce-2  29478  iotaexeu  29517  iotasbc  29518  fnchoice  29596  rfcnnnub  29603  stoweidlem35  29676  stoweidlem57  29698  hash1to3  30081  relopabVD  31360  ax6e2ndeqVD  31368  2uasbanhVD  31370  ax6e2ndeqALT  31390  bnj168  31444  bnj593  31460  bnj607  31632  bnj600  31635  bnj916  31649  bj-exa1  31824  bj-speimfw  31846  bj-axrep2  31951  bj-eumo0  31990  bj-snsetex  32060  bj-snglss  32067  bj-snglex  32070  bj-ccinftydisj  32137
  Copyright terms: Public domain W3C validator