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

Theorem eximi 1566
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 1565 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1538 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531
This theorem is referenced by:  2eximi  1567  exsimpl  1582  19.29r2  1588  19.29x  1589  19.40  1599  19.40-2  1600  exlimiv  1624  speimfw  1635  sbimi  1642  exlimivOLD  1683  19.12  1746  equs4  1912  exdistrf  1924  equvini  1940  equs45f  1942  sbequi  2012  eumo0  2180  euan  2213  eupickb  2221  2eu2ex  2230  darii  2255  barbari  2257  festino  2261  baroco  2262  cesaro  2263  camestros  2264  datisi  2265  disamis  2266  felapton  2269  darapti  2270  dimatis  2272  fresison  2273  calemos  2274  fesapo  2275  bamalip  2276  rexex  2615  reximi2  2662  cgsexg  2832  gencbvex  2843  vtoclf  2850  vtocl3  2853  eqvinc  2908  axrep2  4149  bm1.3ii  4160  ax9vsep  4161  axnul  4164  nalset  4167  notzfaus  4201  el  4208  dtru  4217  dvdemo1  4226  dvdemo2  4227  axpr  4229  snnex  4540  eusv2nf  4548  imassrn  5041  dminss  5111  imainss  5112  iotaex  5252  fv3  5557  ssimaex  5600  dffv2  5608  exfo  5694  zfrep6  5764  oprabid  5898  frxp  6241  tz7.48-1  6471  enssdom  6902  fineqvlem  7093  infcntss  7146  inf1  7339  infeq5  7354  omex  7360  rankuni  7551  scott0  7572  bnd  7578  acni3  7690  finacn  7693  acnnum  7695  dfac3  7764  dfac4  7765  dfac9  7778  kmlem1  7792  kmlem2  7793  cflm  7892  cfcof  7916  axdc4lem  8097  axcclem  8099  ac6c4  8124  ac6c5  8125  ac6s  8127  ac6s2  8129  ac6s3  8130  ac6s5  8134  axdclem2  8163  brdom3  8169  brdom5  8170  brdom4  8171  axpowndlem2  8236  grothomex  8467  nqpr  8654  ltexprlem4  8679  reclem2pr  8688  isssc  13713  drsdirfi  14088  2ndcsb  17191  fbssint  17549  isfil2  17567  alexsubALTlem3  17759  lpbl  18065  ex-natded9.26-2  20823  eqvincg  23146  rexunirn  23156  ceqsexv2d  23178  19.9d2rf  23198  19.9d2r  23199  0elsiga  23490  fundmpss  24193  axextdfeq  24225  ax13dfeq  24226  axextndbi  24232  snelsingles  24532  exisym1  24935  dstr  25274  gltpntl2  26176  isconcl6ab  26207  heiborlem3  26640  exan3  26821  spsbce-2  27682  iotaexeu  27721  iotasbc  27722  fnchoice  27803  rfcnnnub  27810  stoweidlem14  27866  stoweidlem35  27887  stoweidlem57  27909  stoweidlem59  27911  3v3e3cycl2  28410  relopabVD  28993  a9e2ndeqVD  29001  2uasbanhVD  29003  a9e2ndeqALT  29024  bnj101  29065  bnj168  29074  bnj593  29090  bnj607  29264  bnj600  29267  bnj916  29281  19.12vAUX7  29431  exdistrfNEW7  29482  equviniNEW7  29502  equs4NEW7  29508  sbequiNEW7  29553  equs45fNEW7  29593  19.12OLD7  29640  ax9lem11  29772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator