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

Theorem reximi 3157
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 3155 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061
This theorem is referenced by:  2r19.29  3226  r19.29d2r  3227  r19.40  3235  reu3  3555  2reu5  3577  ssiun  4718  iinss  4727  elsnxp  5863  elunirn  6701  iiner  8022  erovlem  8047  xpf1o  8329  unbnn2  8424  scott0  8964  dfac2b  9204  dfac2OLD  9206  cflm  9325  alephsing  9351  numthcor  9569  zorng  9579  zornn0g  9580  ttukeyg  9592  uniimadom  9619  axgroth3  9906  qextlt  12236  qextle  12237  mptnn0fsuppd  13005  hash2sspr  13471  cshword  13818  rexanre  14371  climi2  14527  climi0  14528  rlimres  14574  lo1res  14575  caurcvgr  14689  caurcvg2  14693  caucvgb  14695  prodmolem2  14948  prodmo  14949  vdwnnlem1  15978  cshwsiun  16080  isnmnd  17564  efgrelexlemb  18429  nn0gsumfz0  18647  pmatcollpw2lem  20861  eltg2b  21043  neiptopuni  21214  neiptopnei  21216  ordtbas2  21275  lmcvg  21346  cnprest  21373  lmcnp  21388  nrmsep2  21440  bwth  21493  1stcfb  21528  islly2  21567  llycmpkgen  21635  txbas  21650  tx1stc  21733  cnextcn  22150  tmdcn2  22172  utoptop  22317  ucnima  22364  cfiluweak  22378  metrest  22608  metust  22642  cfilucfil  22643  metustbl  22650  xrhmeo  23024  cmetcaulem  23365  iundisj  23606  limcresi  23940  elply2  24243  aalioulem2  24379  ulmf  24427  lgamucov2  25056  2sqlem7  25440  pntrsumbnd  25546  istrkg2ld  25650  tgisline  25813  umgr2edgneu  26384  umgr3v3e3cycl  27462  eucrctshift  27521  1to3vfriendship  27561  2pthfrgrrn  27562  grpoidval  27824  grporcan  27829  grpoinveu  27830  iundisjf  29850  xlt2addrd  29972  xrofsup  29982  iundisjfi  30004  rhmdvdsr  30265  tpr2rico  30405  esumc  30560  esumfsup  30579  esumpcvgval  30587  hasheuni  30594  esumiun  30603  voliune  30739  volfiniune  30740  dya2icoseg2  30787  dya2iocnei  30791  dya2iocuni  30792  omssubaddlem  30808  omssubadd  30809  afsval  31200  bnj31  31236  bnj1239  31324  bnj900  31447  bnj906  31448  bnj1398  31550  bnj1498  31577  nosupno  32293  nosupfv  32296  colinearex  32611  segcon2  32656  opnrebl2  32759  sdclem2  33960  heibor1lem  34030  grpomndo  34096  prtlem9  34820  prtlem11  34822  prter1  34835  prter2  34837  hl2at  35361  cvrval4N  35370  athgt  35412  1dimN  35427  lhpexnle  35962  lhpexle1  35964  cdlemftr2  36522  cdlemftr1  36523  cdlemftr0  36524  cdlemg5  36561  cdlemg33c0  36658  mapdrvallem2  37601  eldiophb  37998  rmxyelqirr  38152  hbtlem1  38370  hbtlem7  38372  ss2iundf  38626  iinssf  39976  founiiun  40007  founiiun0  40024  climuzlem  40613  stirlinglem13  40940  fourierdlem112  41072  reuan  41851  2reu2rex  41854  gbogbow  42320  sbgoldbo  42351
  Copyright terms: Public domain W3C validator