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

Theorem reximi 2844
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 2842 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-ral 2741  df-rex 2742
This theorem is referenced by:  r19.29d2r  2884  r19.40  2892  reu3  3170  2reu5  3188  ssiun  4233  iinss  4242  elunirn  5989  iiner  7193  erovlem  7217  xpf1o  7494  unbnn2  7590  scott0  8114  dfac2  8321  cflm  8440  alephsing  8466  numthcor  8684  zorng  8694  zornn0g  8695  ttukeyg  8707  uniimadom  8729  axgroth3  9019  qextlt  11194  qextle  11195  cshword  12449  rexanre  12855  climi2  13010  climi0  13011  rlimres  13057  lo1res  13058  caurcvgr  13172  caurcvg2  13176  caucvgb  13178  vdwnnlem1  14077  cshwsiun  14147  efgrelexlemb  16268  eltg2b  18586  neiptopuni  18756  neiptopnei  18758  ordtbas2  18817  lmcvg  18888  cnprest  18915  lmcnp  18930  nrmsep2  18982  bwth  19035  1stcfb  19071  islly2  19110  llycmpkgen  19147  txbas  19162  tx1stc  19245  cnextcn  19661  tmdcn2  19682  utoptop  19831  ucnima  19878  cfiluweak  19892  metrest  20121  metustOLD  20164  metust  20165  cfilucfilOLD  20166  cfilucfil  20167  metustblOLD  20177  metustbl  20178  xrhmeo  20540  cmetcaulem  20821  iundisj  21051  limcresi  21382  elply2  21686  aalioulem2  21821  ulmf  21869  2sqlem7  22731  pntrsumbnd  22837  tgisline  23056  usgra2edg1  23324  3v3e3cycl1  23552  grpoidval  23725  grporcan  23730  grpoinveu  23731  grpomndo  23855  iundisjf  25953  xlt2addrd  26073  xrge0infss  26075  xrofsup  26077  iundisjfi  26102  rhmdvdsr  26308  tpr2rico  26364  esumc  26527  esumfsup  26541  esumpcvgval  26549  hasheuni  26556  voliune  26667  volfiniune  26668  dya2icoseg2  26715  dya2iocnei  26719  dya2iocuni  26720  afsval  27017  lgamucov2  27047  prodmolem2  27470  prodmo  27471  colinearex  28113  segcon2  28158  opnrebl2  28542  sdclem2  28664  heibor1lem  28734  2r19.29  29025  prtlem9  29035  prtlem11  29037  prter1  29050  prter2  29052  eldiophb  29121  rmxyelqirr  29277  hbtlem1  29505  hbtlem7  29507  stirlinglem13  29907  reuan  30030  2reu2rex  30033  wwlkn0  30349  1to3vfriendship  30626  2pthfrgrarn  30627  nn0gsumfz0  30838  scmatid  30921  pmatcollpw2lem  31120  bnj31  31804  bnj1239  31895  bnj900  32018  bnj906  32019  bnj1398  32121  bnj1498  32148  hl2at  33145  cvrval4N  33154  athgt  33196  1dimN  33211  lhpexnle  33746  lhpexle1  33748  cdlemftr2  34306  cdlemftr1  34307  cdlemftr0  34308  cdlemg5  34345  cdlemg33c0  34442  mapdrvallem2  35386
  Copyright terms: Public domain W3C validator