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

Theorem reximi 2932
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 2930 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  r19.29d2r  3004  r19.40  3012  reu3  3293  2reu5  3312  ssiun  4367  iinss  4376  elunirn  6151  iiner  7383  erovlem  7407  xpf1o  7679  unbnn2  7777  scott0  8304  dfac2  8511  cflm  8630  alephsing  8656  numthcor  8874  zorng  8884  zornn0g  8885  ttukeyg  8897  uniimadom  8919  axgroth3  9209  qextlt  11402  qextle  11403  mptnn0fsuppd  12072  cshword  12725  rexanre  13142  climi2  13297  climi0  13298  rlimres  13344  lo1res  13345  caurcvgr  13459  caurcvg2  13463  caucvgb  13465  vdwnnlem1  14372  cshwsiun  14442  efgrelexlemb  16574  nn0gsumfz0  16816  pmatcollpw2lem  19073  eltg2b  19255  neiptopuni  19425  neiptopnei  19427  ordtbas2  19486  lmcvg  19557  cnprest  19584  lmcnp  19599  nrmsep2  19651  bwth  19704  1stcfb  19740  islly2  19779  llycmpkgen  19816  txbas  19831  tx1stc  19914  cnextcn  20330  tmdcn2  20351  utoptop  20500  ucnima  20547  cfiluweak  20561  metrest  20790  metustOLD  20833  metust  20834  cfilucfilOLD  20835  cfilucfil  20836  metustblOLD  20846  metustbl  20847  xrhmeo  21209  cmetcaulem  21490  iundisj  21721  limcresi  22052  elply2  22356  aalioulem2  22491  ulmf  22539  2sqlem7  23401  pntrsumbnd  23507  istrkg2ld  23614  tgisline  23749  usgra2edg1  24087  3v3e3cycl1  24348  wwlkn0  24393  1to3vfriendship  24712  2pthfrgrarn  24713  grpoidval  24922  grporcan  24927  grpoinveu  24928  grpomndo  25052  iundisjf  27149  xlt2addrd  27274  xrge0infss  27276  xrofsup  27278  iundisjfi  27297  rhmdvdsr  27499  tpr2rico  27558  esumc  27730  esumfsup  27744  esumpcvgval  27752  hasheuni  27759  voliune  27869  volfiniune  27870  dya2icoseg2  27917  dya2iocnei  27921  dya2iocuni  27922  afsval  28219  lgamucov2  28249  prodmolem2  28672  prodmo  28673  colinearex  29315  segcon2  29360  opnrebl2  29744  sdclem2  29866  heibor1lem  29936  2r19.29  30227  prtlem9  30237  prtlem11  30239  prter1  30252  prter2  30254  eldiophb  30322  rmxyelqirr  30478  hbtlem1  30704  hbtlem7  30706  stirlinglem13  31414  fourierdlem112  31547  reuan  31680  2reu2rex  31683  usg2edgneu  31907  bnj31  32870  bnj1239  32961  bnj900  33084  bnj906  33085  bnj1398  33187  bnj1498  33214  hl2at  34219  cvrval4N  34228  athgt  34270  1dimN  34285  lhpexnle  34820  lhpexle1  34822  cdlemftr2  35380  cdlemftr1  35381  cdlemftr0  35382  cdlemg5  35419  cdlemg33c0  35516  mapdrvallem2  36460
  Copyright terms: Public domain W3C validator