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

Theorem reximi 2922
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 2920 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  r19.29d2r  2997  r19.40  3005  reu3  3286  2reu5  3305  ssiun  4357  iinss  4366  elunirn  6138  iiner  7375  erovlem  7399  xpf1o  7672  unbnn2  7769  scott0  8295  dfac2  8502  cflm  8621  alephsing  8647  numthcor  8865  zorng  8875  zornn0g  8876  ttukeyg  8888  uniimadom  8910  axgroth3  9198  qextlt  11405  qextle  11406  mptnn0fsuppd  12089  cshword  12756  rexanre  13264  climi2  13419  climi0  13420  rlimres  13466  lo1res  13467  caurcvgr  13581  caurcvg2  13585  caucvgb  13587  prodmolem2  13827  prodmo  13828  vdwnnlem1  14600  cshwsiun  14671  isnmnd  16126  efgrelexlemb  16970  nn0gsumfz0  17211  pmatcollpw2lem  19448  eltg2b  19630  neiptopuni  19801  neiptopnei  19803  ordtbas2  19862  lmcvg  19933  cnprest  19960  lmcnp  19975  nrmsep2  20027  bwth  20080  1stcfb  20115  islly2  20154  llycmpkgen  20222  txbas  20237  tx1stc  20320  cnextcn  20736  tmdcn2  20757  utoptop  20906  ucnima  20953  cfiluweak  20967  metrest  21196  metustOLD  21239  metust  21240  cfilucfilOLD  21241  cfilucfil  21242  metustblOLD  21252  metustbl  21253  xrhmeo  21615  cmetcaulem  21896  iundisj  22127  limcresi  22458  elply2  22762  aalioulem2  22898  ulmf  22946  2sqlem7  23846  pntrsumbnd  23952  istrkg2ld  24059  tgisline  24211  usgra2edg1  24588  3v3e3cycl1  24849  wwlkn0  24894  1to3vfriendship  25213  2pthfrgrarn  25214  grpoidval  25419  grporcan  25424  grpoinveu  25425  grpomndo  25549  iundisjf  27662  elsnxp  27687  xlt2addrd  27812  xrge0infss  27814  xrofsup  27819  iundisjfi  27838  rhmdvdsr  28046  tpr2rico  28132  esumc  28283  esumfsup  28302  esumpcvgval  28310  hasheuni  28317  esumiun  28326  voliune  28441  volfiniune  28442  dya2icoseg2  28489  dya2iocnei  28493  dya2iocuni  28494  omssubaddlem  28510  omssubadd  28511  afsval  28818  lgamucov2  28848  colinearex  29941  segcon2  29986  opnrebl2  30382  sdclem2  30478  heibor1lem  30548  2r19.29  30838  prtlem9  30848  prtlem11  30850  prter1  30863  prter2  30865  eldiophb  30932  rmxyelqirr  31088  hbtlem1  31316  hbtlem7  31318  stirlinglem13  32110  fourierdlem112  32243  reuan  32427  2reu2rex  32430  cshword2  32684  usg2edgneu  32803  bnj31  34192  bnj1239  34284  bnj900  34407  bnj906  34408  bnj1398  34510  bnj1498  34537  hl2at  35545  cvrval4N  35554  athgt  35596  1dimN  35611  lhpexnle  36146  lhpexle1  36148  cdlemftr2  36708  cdlemftr1  36709  cdlemftr0  36710  cdlemg5  36747  cdlemg33c0  36844  mapdrvallem2  37788
  Copyright terms: Public domain W3C validator