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

Theorem eximi 1563
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 1562 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1535 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  2eximi  1564  exsimpl  1579  19.29r2  1585  19.29x  1586  19.40  1596  19.40-2  1597  speimfw  1626  sbimi  1633  exlimiv  1666  19.12  1734  equs4  1899  exdistrf  1911  equvini  1927  equs45f  1929  sbequi  1999  eumo0  2167  euan  2200  eupickb  2208  2eu2ex  2217  darii  2242  barbari  2244  festino  2248  baroco  2249  cesaro  2250  camestros  2251  datisi  2252  disamis  2253  felapton  2256  darapti  2257  dimatis  2259  fresison  2260  calemos  2261  fesapo  2262  bamalip  2263  rexex  2602  reximi2  2649  cgsexg  2819  gencbvex  2830  vtoclf  2837  vtocl3  2840  eqvinc  2895  axrep2  4133  bm1.3ii  4144  ax9vsep  4145  axnul  4148  nalset  4151  notzfaus  4185  el  4192  dtru  4201  dvdemo1  4210  dvdemo2  4211  axpr  4213  snnex  4524  eusv2nf  4532  imassrn  5025  dminss  5095  imainss  5096  iotaex  5236  fv3  5541  ssimaex  5584  dffv2  5592  exfo  5678  zfrep6  5748  oprabid  5882  frxp  6225  tz7.48-1  6455  enssdom  6886  fineqvlem  7077  infcntss  7130  inf1  7323  infeq5  7338  omex  7344  rankuni  7535  scott0  7556  bnd  7562  acni3  7674  finacn  7677  acnnum  7679  dfac3  7748  dfac4  7749  dfac9  7762  kmlem1  7776  kmlem2  7777  cflm  7876  cfcof  7900  axdc4lem  8081  axcclem  8083  ac6c4  8108  ac6c5  8109  ac6s  8111  ac6s2  8113  ac6s3  8114  ac6s5  8118  axdclem2  8147  brdom3  8153  brdom5  8154  brdom4  8155  axpowndlem2  8220  grothomex  8451  nqpr  8638  ltexprlem4  8663  reclem2pr  8672  isssc  13697  drsdirfi  14072  2ndcsb  17175  fbssint  17533  isfil2  17551  alexsubALTlem3  17743  lpbl  18049  ex-natded9.26-2  20807  eqvincg  23130  rexunirn  23140  ceqsexv2d  23162  19.9d2rf  23182  19.9d2r  23183  0elsiga  23475  fundmpss  24122  axextdfeq  24154  ax13dfeq  24155  axextndbi  24161  snelsingles  24461  exisym1  24863  dstr  25171  gltpntl2  26073  isconcl6ab  26104  heiborlem3  26537  exan3  26718  spsbce-2  27579  iotaexeu  27618  iotasbc  27619  fnchoice  27700  rfcnnnub  27707  stoweidlem14  27763  stoweidlem35  27784  stoweidlem57  27806  stoweidlem59  27808  relopabVD  28677  a9e2ndeqVD  28685  2uasbanhVD  28687  a9e2ndeqALT  28708  bnj101  28749  bnj168  28758  bnj593  28774  bnj607  28948  bnj600  28951  bnj916  28965  ax9lem11  29150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator