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

Theorem reximi 2813
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
Hypothesis
Ref Expression
reximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
reximi  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )

Proof of Theorem reximi
StepHypRef Expression
1 reximi.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32reximia 2811 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   E.wrex 2706
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-an 371  df-ex 1590  df-ral 2710  df-rex 2711
This theorem is referenced by:  r19.29d2r  2853  r19.40  2861  reu3  3138  2reu5  3156  ssiun  4200  iinss  4209  elunirnALT  5957  iiner  7160  erovlem  7184  xpf1o  7461  unbnn2  7557  scott0  8081  dfac2  8288  cflm  8407  alephsing  8433  numthcor  8651  zorng  8661  zornn0g  8662  ttukeyg  8674  uniimadom  8696  axgroth3  8985  qextlt  11160  qextle  11161  cshword  12411  rexanre  12817  climi2  12972  climi0  12973  rlimres  13019  lo1res  13020  caurcvgr  13134  caurcvg2  13138  caucvgb  13140  vdwnnlem1  14038  cshwsiun  14108  efgrelexlemb  16226  eltg2b  18405  neiptopuni  18575  neiptopnei  18577  ordtbas2  18636  lmcvg  18707  cnprest  18734  lmcnp  18749  nrmsep2  18801  bwth  18854  1stcfb  18890  islly2  18929  llycmpkgen  18966  txbas  18981  tx1stc  19064  cnextcn  19480  tmdcn2  19501  utoptop  19650  ucnima  19697  cfiluweak  19711  metrest  19940  metustOLD  19983  metust  19984  cfilucfilOLD  19985  cfilucfil  19986  metustblOLD  19996  metustbl  19997  xrhmeo  20359  cmetcaulem  20640  iundisj  20870  limcresi  21201  elply2  21548  aalioulem2  21683  ulmf  21731  2sqlem7  22593  pntrsumbnd  22699  tgisline  22905  usgra2edg1  23124  3v3e3cycl1  23352  grpoidval  23525  grporcan  23530  grpoinveu  23531  grpomndo  23655  iundisjf  25754  xlt2addrd  25875  xrofsup  25877  iundisjfi  25902  rhmdvdsr  26138  tpr2rico  26195  esumc  26358  esumfsup  26372  esumpcvgval  26380  hasheuni  26387  voliune  26498  volfiniune  26499  dya2icoseg2  26546  dya2iocnei  26550  dya2iocuni  26551  afsval  26842  lgamucov2  26872  prodmolem2  27294  prodmo  27295  colinearex  27937  segcon2  27982  opnrebl2  28357  sdclem2  28479  heibor1lem  28549  2r19.29  28841  prtlem9  28851  prtlem11  28853  prter1  28866  prter2  28868  eldiophb  28937  rmxyelqirr  29093  hbtlem1  29321  hbtlem7  29323  stirlinglem13  29724  reuan  29847  2reu2rex  29850  wwlkn0  30166  1to3vfriendship  30443  2pthfrgrarn  30444  bnj31  31407  bnj1239  31498  bnj900  31621  bnj906  31622  bnj1398  31724  bnj1498  31751  hl2at  32619  cvrval4N  32628  athgt  32670  1dimN  32685  lhpexnle  33220  lhpexle1  33222  cdlemftr2  33780  cdlemftr1  33781  cdlemftr0  33782  cdlemg5  33819  cdlemg33c0  33916  mapdrvallem2  34860
  Copyright terms: Public domain W3C validator