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

Theorem r19.21bi 3120
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.)
Hypothesis
Ref Expression
r19.21bi.1 (𝜑 → ∀𝑥𝐴 𝜓)
Assertion
Ref Expression
r19.21bi ((𝜑𝑥𝐴) → 𝜓)

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . 3 (𝜑 → ∀𝑥𝐴 𝜓)
2 rsp 3117 . . 3 (∀𝑥𝐴 𝜓 → (𝑥𝐴𝜓))
31, 2syl 17 . 2 (𝜑 → (𝑥𝐴𝜓))
43imp 395 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3101
This theorem is referenced by:  r19.21be  3121  rspec2  3122  rspec3  3123  ralxfr2d  5079  fvmptelrn  6601  f1oresrab  6613  isoselem  6811  boxcutc  8184  xpf1o  8357  fineqvlem  8409  indexfi  8509  dffi3  8572  suppr  8612  supiso  8616  infpr  8644  ordtypelem9  8666  brwdom3  8722  xpwdomg  8725  ixpiunwdom  8731  infxpenc2lem1  9121  hsmexlem4  9532  gchina  9802  wunom  9823  prcdnq  10096  prnmax  10098  dedekind  10481  dedekindle  10482  monoord2  13051  limsupgre  14431  limsupbnd1  14432  limsupbnd2  14433  climmpt2  14523  rlimcld2  14528  rlimmptrcl  14557  lo1mptrcl  14571  o1mptrcl  14572  climsup  14619  sumpr  14696  sumtp  14697  fsum2dlem  14720  fsumiun  14771  fprod2dlem  14927  iserodd  15753  vdwlem1  15898  vdwlem6  15903  vdwnnlem3  15914  imasvscafn  16398  fuciso  16835  evlfcl  17063  yonedainv  17122  acsmapd  17379  prdsmndd  17524  psgnunilem5  18111  gsummpt1n0  18561  dprdspan  18624  ablfaclem2  18683  srgi  18709  srgrz  18724  srglz  18725  issrngd  19061  psrbaglesupp  19573  psrbagcon  19576  psrass1lem  19582  evlslem2  19716  mpfind  19740  gsumsmonply1  19877  gsummoncoe1  19878  evl1gsummon  19933  frgpcyg  20125  frlmgsum  20318  uvcresum  20339  cpmatmcllem  20733  neiptoptop  21146  neiptopnei  21147  ordtrest2lem  21218  cncmp  21406  1stckgenlem  21567  ptcld  21627  dfac14  21632  txcnp  21634  ptcnplem  21635  ptcnp  21636  ptcn  21641  pthaus  21652  xkococnlem  21673  xkococn  21674  cnmpt11  21677  cnmpt1t  21679  cnmpt12  21681  cnmptkp  21694  cnmptk1  21695  cnmptkk  21697  cnmptk1p  21699  cnmptk2  21700  cnmpt2k  21702  xpstopnlem1  21823  cnpflfi  22013  ptcmplem2  22067  cnextcn  22081  cnextfres1  22082  cnmpt1plusg  22101  cnmpt2plusg  22102  cnmpt1vsca  22207  cnmpt2vsca  22208  ustfilxp  22226  utoptop  22248  restutop  22251  restutopopn  22252  ucncn  22299  cfilufg  22307  trcfilu  22308  psmet0  22323  psmettri2  22324  prdsxmetlem  22383  prdsbl  22506  prdsxmslem2  22544  psmetutop  22582  cnmpt1ds  22855  cnmpt2ds  22856  cncfmpt2ss  22928  bndth  22967  cnmpt1ip  23255  cnmpt2ip  23256  iscmet3lem2  23300  cmetcusp1  23359  rrxcph  23391  ovoliunlem1  23482  ovoliunlem3  23484  ovoliun  23485  ovoliun2  23486  ovolscalem1  23493  volfiniun  23527  uniioombllem4  23566  mbfmptcl  23616  mbfeqalem1  23621  mbfres2  23625  ismbf3d  23634  mbfsup  23644  mbfinf  23645  mbflim  23648  itg1ge0  23666  itg1mulc  23684  i1fposd  23687  itg1climres  23694  mbfi1fseqlem4  23698  itg2lea  23724  itg2splitlem  23728  itg2split  23729  itg2monolem1  23730  itg2mono  23733  itg2i1fseqle  23734  itg2i1fseq  23735  itg2addlem  23738  itg2cnlem1  23741  itgeqa  23793  itgss3  23794  itgfsum  23806  itgabs  23814  itggt0  23821  dvmptcl  23935  dvmptco  23948  dvlipcn  23970  dvle  23983  dvfsumle  23997  dvfsumge  23998  dvfsumabs  23999  dvmptrecl  24000  dvfsumlem2  24003  itgparts  24023  itgsubstlem  24024  itgsubst  24025  coeeulem  24193  dgrlem  24198  dgrlb  24205  coeaddlem  24218  coecj  24247  ulmss  24364  ulmdvlem2  24368  logtayl  24619  leibpi  24882  xrlimcnp  24908  o1cxp  24914  jensen  24928  lgambdd  24976  wilthlem2  25008  sqff1o  25121  fsumdvdscom  25124  fsumdvdsmul  25134  dchrmulcl  25187  dchrmulid2  25190  dchrinv  25199  dchrisumlem3  25393  dchrvmasumlem2  25400  ostth1  25535  ercgrg  25625  f1otrg  25964  f1otrge  25965  ubthlem2  28054  fmptcof2  29783  disjdsct  29806  fprodex01  29897  ressprs  29979  oduprs  29980  archiabl  30076  lmodslmd  30081  txomap  30225  qtophaus  30227  locfinreflem  30231  ordtrest2NEWlem  30292  lmdvg  30323  prodindf  30409  esumcl  30416  esumeq2d  30423  esumnul  30434  hasheuni  30471  esumcvg  30472  esumcvgre  30477  insiga  30524  ldsysgenld  30547  ldgenpisyslem1  30550  measvunilem  30599  measvunilem0  30600  measdivcstOLD  30611  cntmeas  30613  voliune  30616  volfiniune  30617  1stmbfm  30646  2ndmbfm  30647  omssubadd  30686  difelcarsg  30696  inelcarsg  30697  eulerpartlems  30746  eulerpartlemsv3  30747  eulerpartlemgvv  30762  dstrvprob  30857  hashreprin  31022  reprgt  31023  breprexplemc  31034  circlemeth  31042  hgt750lema  31059  tgoldbachgtd  31064  bnj93  31254  bnj518  31277  bnj1489  31445  subfacp1lem3  31485  subfacp1lem5  31487  erdszelem8  31501  ptpconn  31536  resconn  31549  cvmliftmolem2  31585  cvmlift2lem11  31616  cvmliftphtlem  31620  mclsax  31787  conway  32229  slerec  32242  fin2so  33707  poimirlem18  33738  poimirlem21  33741  mblfinlem2  33758  itgabsnc  33789  itggt0cn  33792  prdsbnd  33901  prdstotbnd  33902  prdsbnd2  33903  rrnequiv  33943  eqlkr3  34879  dih1dimatlem  37107  fnwe2lem1  38118  imo72b2  38972  rfcnnnub  39686  disjxp1  39728  fompt  39865  fvixp2  39874  dmrelrnrel  39903  suplesup  40032  infxr  40060  monoord2xrv  40190  climinf  40315  climsuse  40317  mullimc  40325  limccog  40329  mullimcf  40332  limcperiod  40337  limcleqr  40353  neglimc  40356  0ellimcdiv  40358  limclner  40360  limsuppnfdlem  40410  limsupubuzlem  40421  xlimmnfvlem2  40536  xlimpnfvlem2  40540  climxlim2lem  40548  dvdivbd  40615  ioodvbdlimc1lem1  40623  dvnprodlem2  40639  iblsplit  40658  stoweidlem5  40698  stoweidlem16  40709  stoweidlem21  40714  stoweidlem24  40717  stoweidlem25  40718  stoweidlem28  40721  stoweidlem31  40724  stoweidlem41  40734  stoweidlem42  40735  stoweidlem44  40737  stoweidlem45  40738  stoweidlem48  40741  stoweidlem51  40744  stoweidlem54  40747  stoweidlem57  40750  stoweidlem60  40753  stoweidlem62  40755  stirlinglem5  40771  dirkercncflem3  40798  fourierdlem11  40811  fourierdlem12  40812  fourierdlem14  40814  fourierdlem15  40815  fourierdlem31  40831  fourierdlem34  40834  fourierdlem41  40841  fourierdlem48  40847  fourierdlem49  40848  fourierdlem50  40849  fourierdlem54  40853  fourierdlem69  40868  fourierdlem73  40872  fourierdlem74  40873  fourierdlem75  40874  fourierdlem76  40875  fourierdlem79  40878  fourierdlem80  40879  fourierdlem81  40880  fourierdlem92  40891  fourierdlem93  40892  fourierdlem94  40893  fourierdlem97  40896  fourierdlem103  40902  fourierdlem104  40903  fourierdlem111  40910  fourierdlem113  40912  etransclem32  40959  subsaliuncllem  41051  sge0rpcpnf  41114  caragendifcl  41207  iinhoiicclem  41366  pimdecfgtioc  41404  issmfgtlem  41443
  Copyright terms: Public domain W3C validator