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

Theorem reximi 3209
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 3208 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wrex 3110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115
This theorem is referenced by:  r19.29r  3220  2r19.29  3293  r19.29d2r  3294  r19.29vva  3295  r19.35  3298  r19.40  3302  2reu2rex  3380  reu3  3669  2reu5  3700  reuan  3828  ssiun  4936  iinss  4946  elsnxp  6114  elunirn  6992  iiner  8356  erovlem  8380  xpf1o  8667  unbnn2  8763  scott0  9303  dfac2b  9545  cflm  9665  alephsing  9691  numthcor  9909  zorng  9919  zornn0g  9920  ttukeyg  9932  uniimadom  9959  axgroth3  10246  qextlt  12588  qextle  12589  mptnn0fsuppd  13365  hashgt23el  13785  hash2sspr  13846  cshword  14148  rexanre  14702  climi2  14864  climi0  14865  rlimres  14911  lo1res  14912  caurcvgr  15026  caurcvg2  15030  caucvgb  15032  prodmolem2  15285  prodmo  15286  vdwnnlem1  16325  cshwsiun  16429  isnmnd  17911  efgrelexlemb  18872  nn0gsumfz0  19102  ablsimpgfind  19229  pmatcollpw2lem  21386  eltg2b  21568  neiptopuni  21739  neiptopnei  21741  ordtbas2  21800  lmcvg  21871  cnprest  21898  lmcnp  21913  nrmsep2  21965  bwth  22019  1stcfb  22054  islly2  22093  llycmpkgen  22161  txbas  22176  tx1stc  22259  cnextcn  22676  tmdcn2  22698  utoptop  22844  ucnima  22891  cfiluweak  22905  metrest  23135  metust  23169  cfilucfil  23170  metustbl  23177  xrhmeo  23555  cmetcaulem  23896  iundisj  24156  limcresi  24492  elply2  24797  aalioulem2  24933  ulmf  24981  lgamucov2  25628  2sqlem7  26012  2sqreultblem  26036  2sqreunnltblem  26039  pntrsumbnd  26154  istrkg2ld  26258  tgisline  26425  umgr2edgneu  27008  umgr3v3e3cycl  27973  eucrctshift  28032  1to3vfriendship  28070  2pthfrgrrn  28071  grpoidval  28300  grporcan  28305  grpoinveu  28306  iunrnmptss  30333  iundisjf  30356  xlt2addrd  30512  xrofsup  30522  iundisjfi  30549  rhmdvdsr  30946  tpr2rico  31269  esumc  31424  esumfsup  31443  esumpcvgval  31451  hasheuni  31458  esumiun  31467  voliune  31602  volfiniune  31603  dya2icoseg2  31650  dya2iocnei  31654  dya2iocuni  31655  omssubaddlem  31671  omssubadd  31672  afsval  32056  bnj31  32103  bnj1239  32191  bnj900  32315  bnj906  32316  bnj1398  32420  bnj1498  32447  satfvsuclem1  32720  satfv1  32724  satfvsucsuc  32726  nosupno  33317  nosupfv  33320  colinearex  33635  segcon2  33680  opnrebl2  33783  nlpfvineqsn  34827  fvineqsneq  34830  pibt2  34835  sdclem2  35179  heibor1lem  35246  grpomndo  35312  prtlem9  36159  prter1  36174  prter2  36176  hl2at  36700  cvrval4N  36709  athgt  36751  1dimN  36766  lhpexnle  37301  lhpexle1  37303  cdlemftr2  37861  cdlemftr1  37862  cdlemftr0  37863  cdlemg5  37900  cdlemg33c0  37997  mapdrvallem2  38940  sn-negex  39547  sn-negex2  39548  eldiophb  39691  rmxyelqirr  39844  hbtlem1  40060  hbtlem7  40062  ss2iundf  40353  mnupwd  40968  iinssf  41768  founiiun  41796  founiiun0  41810  climuzlem  42378  stirlinglem13  42721  fourierdlem112  42853  2reuimp0  43663  2reuimp  43664  gbogbow  44267  sbgoldbo  44298
  Copyright terms: Public domain W3C validator