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

Theorem reximi 2909
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 2907 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797
This theorem is referenced by:  r19.29d2r  2984  r19.40  2992  reu3  3273  2reu5  3292  ssiun  4353  iinss  4362  elunirn  6144  iiner  7381  erovlem  7405  xpf1o  7677  unbnn2  7775  scott0  8302  dfac2  8509  cflm  8628  alephsing  8654  numthcor  8872  zorng  8882  zornn0g  8883  ttukeyg  8895  uniimadom  8917  axgroth3  9207  qextlt  11406  qextle  11407  mptnn0fsuppd  12078  cshword  12736  rexanre  13153  climi2  13308  climi0  13309  rlimres  13355  lo1res  13356  caurcvgr  13470  caurcvg2  13474  caucvgb  13476  vdwnnlem1  14385  cshwsiun  14456  isnmnd  15793  efgrelexlemb  16637  nn0gsumfz0  16882  pmatcollpw2lem  19145  eltg2b  19327  neiptopuni  19497  neiptopnei  19499  ordtbas2  19558  lmcvg  19629  cnprest  19656  lmcnp  19671  nrmsep2  19723  bwth  19776  1stcfb  19812  islly2  19851  llycmpkgen  19919  txbas  19934  tx1stc  20017  cnextcn  20433  tmdcn2  20454  utoptop  20603  ucnima  20650  cfiluweak  20664  metrest  20893  metustOLD  20936  metust  20937  cfilucfilOLD  20938  cfilucfil  20939  metustblOLD  20949  metustbl  20950  xrhmeo  21312  cmetcaulem  21593  iundisj  21824  limcresi  22155  elply2  22459  aalioulem2  22594  ulmf  22642  2sqlem7  23510  pntrsumbnd  23616  istrkg2ld  23723  tgisline  23872  usgra2edg1  24248  3v3e3cycl1  24509  wwlkn0  24554  1to3vfriendship  24873  2pthfrgrarn  24874  grpoidval  25083  grporcan  25088  grpoinveu  25089  grpomndo  25213  iundisjf  27313  xlt2addrd  27443  xrge0infss  27445  xrofsup  27447  iundisjfi  27466  rhmdvdsr  27674  tpr2rico  27760  esumc  27928  esumfsup  27942  esumpcvgval  27950  hasheuni  27957  voliune  28067  volfiniune  28068  dya2icoseg2  28115  dya2iocnei  28119  dya2iocuni  28120  afsval  28417  lgamucov2  28447  prodmolem2  29035  prodmo  29036  colinearex  29678  segcon2  29723  opnrebl2  30107  sdclem2  30203  heibor1lem  30273  2r19.29  30563  prtlem9  30573  prtlem11  30575  prter1  30588  prter2  30590  eldiophb  30658  rmxyelqirr  30814  hbtlem1  31040  hbtlem7  31042  stirlinglem13  31753  fourierdlem112  31886  reuan  32019  2reu2rex  32022  usg2edgneu  32246  bnj31  33480  bnj1239  33571  bnj900  33694  bnj906  33695  bnj1398  33797  bnj1498  33824  hl2at  34831  cvrval4N  34840  athgt  34882  1dimN  34897  lhpexnle  35432  lhpexle1  35434  cdlemftr2  35994  cdlemftr1  35995  cdlemftr0  35996  cdlemg5  36033  cdlemg33c0  36130  mapdrvallem2  37074
  Copyright terms: Public domain W3C validator