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

Theorem reximi 2993
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
Hypothesis
Ref Expression
reximi.1 (𝜑𝜓)
Assertion
Ref Expression
reximi (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)

Proof of Theorem reximi
StepHypRef Expression
1 reximi.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32reximia 2991 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  r19.29d2r  3060  r19.40  3068  reu3  3362  2reu5  3382  ssiun  4492  iinss  4501  elsnxp  5579  elsnxpOLD  5580  elunirn  6390  iiner  7683  erovlem  7707  xpf1o  7984  unbnn2  8079  scott0  8609  dfac2  8813  cflm  8932  alephsing  8958  numthcor  9176  zorng  9186  zornn0g  9187  ttukeyg  9199  uniimadom  9222  axgroth3  9509  qextlt  11869  qextle  11870  mptnn0fsuppd  12617  hash2sspr  13076  cshword  13336  rexanre  13882  climi2  14038  climi0  14039  rlimres  14085  lo1res  14086  caurcvgr  14200  caurcvg2  14204  caucvgb  14206  prodmolem2  14452  prodmo  14453  vdwnnlem1  15485  cshwsiun  15592  isnmnd  17069  efgrelexlemb  17934  nn0gsumfz0  18152  pmatcollpw2lem  20348  eltg2b  20521  neiptopuni  20691  neiptopnei  20693  ordtbas2  20752  lmcvg  20823  cnprest  20850  lmcnp  20865  nrmsep2  20917  bwth  20970  1stcfb  21005  islly2  21044  llycmpkgen  21112  txbas  21127  tx1stc  21210  cnextcn  21628  tmdcn2  21650  utoptop  21795  ucnima  21842  cfiluweak  21856  metrest  22086  metust  22120  cfilucfil  22121  metustbl  22128  xrhmeo  22500  cmetcaulem  22838  iundisj  23067  limcresi  23399  elply2  23700  aalioulem2  23836  ulmf  23884  lgamucov2  24509  2sqlem7  24893  pntrsumbnd  24999  istrkg2ld  25103  tgisline  25267  usgra2edg1  25705  3v3e3cycl1  25965  wwlkn0  26010  1to3vfriendship  26328  2pthfrgrarn  26329  grpoidval  26544  grporcan  26549  grpoinveu  26550  iundisjf  28577  xlt2addrd  28706  xrofsup  28716  iundisjfi  28735  rhmdvdsr  28942  tpr2rico  29079  esumc  29233  esumfsup  29252  esumpcvgval  29260  hasheuni  29267  esumiun  29276  voliune  29412  volfiniune  29413  dya2icoseg2  29460  dya2iocnei  29464  dya2iocuni  29465  omssubaddlem  29481  omssubadd  29482  afsval  29795  bnj31  29832  bnj1239  29923  bnj900  30046  bnj906  30047  bnj1398  30149  bnj1498  30176  colinearex  31130  segcon2  31175  opnrebl2  31279  sdclem2  32491  heibor1lem  32561  grpomndo  32627  2r19.29  32943  prtlem9  32950  prtlem11  32952  prter1  32965  prter2  32967  hl2at  33492  cvrval4N  33501  athgt  33543  1dimN  33558  lhpexnle  34093  lhpexle1  34095  cdlemftr2  34655  cdlemftr1  34656  cdlemftr0  34657  cdlemg5  34694  cdlemg33c0  34791  mapdrvallem2  35735  eldiophb  36121  rmxyelqirr  36276  hbtlem1  36495  hbtlem7  36497  ss2iundf  36753  founiiun  38138  founiiun0  38155  stirlinglem13  38762  fourierdlem112  38894  reuan  39612  2reu2rex  39615  gboagbo  39962  cshword2  40084  umgr2edgneu  40422  umgr3v3e3cycl  41332  eucrctshift  41392  1to3vfriendship-av  41432  2pthfrgrrn  41433  fusgreg2wsp  41481
  Copyright terms: Public domain W3C validator