Theorem r19.21bi 3226

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 11-Jun-2023.)

Hypothesis

Ref	Expression
r19.21bi.1	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
r19.21bi	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		rspa 3223	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜓)
3	1, 2	sylan 580	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050

This theorem is referenced by:  r19.21be  3227  rspec2  3253  rspec3  3254  ralxfr2d  5353  fvmptelcdm  7056  fompt  7061  f1oresrab  7070  isoselem  7285  mpoexw  8020  naddsuc2  8627  boxcutc  8877  xpf1o  9065  fineqvlem  9164  indexfi  9258  dffi3  9332  suppr  9373  supiso  9377  infpr  9406  ordtypelem9  9429  brwdom3  9485  xpwdomg  9488  ixpiunwdom  9493  infxpenc2lem1  9927  hsmexlem4  10337  gchina  10608  wunom  10629  prcdnq  10902  prnmax  10904  dedekind  11294  dedekindle  11295  monoord2  13954  limsupgre  15402  limsupbnd1  15403  limsupbnd2  15404  climmpt2  15494  rlimcld2  15499  climsup  15591  sumpr  15669  sumtp  15670  fsum2dlem  15691  fsumiun  15742  fprod2dlem  15901  iserodd  16761  vdwlem1  16907  vdwlem6  16912  vdwnnlem3  16923  imasvscafn  17456  fuciso  17900  evlfcl  18143  yonedainv  18202  oduprs  18221  acsmapd  18475  chnccats1  18546  chnccat  18547  prdsmndd  18693  psgnunilem5  19421  gsummpt1n0  19892  dprdspan  19956  ablfaclem2  20015  srgdilem  20125  srgrz  20140  srglz  20141  issrngd  20786  frgpcyg  21526  psrbaglesupp  21876  psrbagcon  21879  psrbagleadd1  21882  evlslem2  22032  mpfind  22068  psdmul  22107  ply1chr  22248  gsumsmonply1  22249  gsummoncoe1  22250  evl1gsummon  22307  cpmatmcllem  22660  neiptoptop  23073  neiptopnei  23074  ordtrest2lem  23145  cncmp  23334  1stckgenlem  23495  ptcld  23555  dfac14  23560  ptcnplem  23563  pthaus  23580  xkococnlem  23601  xkococn  23602  cnmpt2k  23630  xpstopnlem1  23751  cnpflfi  23941  ptcmplem2  23995  cnextcn  24009  cnextfres1  24010  cnmpt2plusg  24030  cnmpt2vsca  24137  ustfilxp  24155  utoptop  24176  restutop  24179  restutopopn  24180  ucncn  24226  cfilufg  24234  trcfilu  24235  psmet0  24250  psmettri2  24251  prdsxmetlem  24310  prdsbl  24433  prdsxmslem2  24471  psmetutop  24509  cnmpt2ds  24786  bndth  24911  cnmpt2ip  25202  iscmet3lem2  25246  cmetcusp1  25307  rrxcph  25346  ovoliunlem1  25457  ovoliunlem3  25459  ovoliun  25460  ovoliun2  25461  ovolscalem1  25468  volfiniun  25502  uniioombllem4  25541  mbfeqalem1  25596  mbfres2  25600  ismbf3d  25609  mbfsup  25619  mbfinf  25620  mbflim  25623  itg1ge0  25641  itg1mulc  25659  itg1climres  25669  mbfi1fseqlem4  25673  itg2lea  25699  itg2splitlem  25703  itg2split  25704  itg2monolem1  25705  itg2mono  25708  itg2i1fseqle  25709  itg2i1fseq  25710  itg2addlem  25713  itg2cnlem1  25716  itgeqa  25769  itgfsum  25782  itgabs  25790  itggt0  25799  dvlipcn  25953  dvfsumabs  25983  dvfsumlem2  25987  dvfsumlem2OLD  25988  itgsubstlem  26009  coeeulem  26183  dgrlem  26188  dgrlb  26195  coeaddlem  26208  coecj  26238  coecjOLD  26240  ulmss  26360  leibpi  26906  xrlimcnp  26932  o1cxp  26939  jensen  26953  lgambdd  27001  wilthlem2  27033  sqff1o  27146  fsumdvdscom  27149  fsumdvdsmul  27159  fsumdvdsmulOLD  27161  dchrmulcl  27214  dchrmullid  27217  dchrinv  27226  dchrvmasumlem2  27463  ostth1  27598  conway  27767  slerec  27787  ercgrg  28538  f1otrg  28892  f1otrge  28893  ubthlem2  30895  fmptcof2  32684  disjdsct  32731  fprodex01  32855  prodindf  32893  ccatf1  32980  ressprs  32997  mgcf1o  33034  gsumpart  33095  archiabl  33229  lmodslmd  33235  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnsubrunlem2  33279  rhmimaidl  33462  gsummoncoe1fzo  33627  ply1gsumz  33629  vietadeg1  33683  vietalem  33684  fedgmullem2  33736  fedgmul  33737  txomap  33940  qtophaus  33942  locfinreflem  33946  ordtrest2NEWlem  34028  lmdvg  34059  zrhcntr  34085  esumcl  34136  esumeq2d  34143  esumnul  34154  hasheuni  34191  esumcvg  34192  esumcvgre  34197  insiga  34243  ldsysgenld  34266  ldgenpisyslem1  34269  measvunilem  34318  measvunilem0  34319  measdivcstALTV  34331  cntmeas  34332  voliune  34335  volfiniune  34336  1stmbfm  34366  2ndmbfm  34367  omssubadd  34406  difelcarsg  34416  inelcarsg  34417  eulerpartlems  34466  eulerpartlemsv3  34467  eulerpartlemgvv  34482  dstrvprob  34578  hashreprin  34726  reprgt  34727  breprexplemc  34738  circlemeth  34746  hgt750lema  34763  tgoldbachgtd  34768  bnj93  34968  bnj518  34991  bnj1489  35161  fnrelpredd  35196  subfacp1lem3  35325  subfacp1lem5  35327  erdszelem8  35341  ptpconn  35376  resconn  35389  cvmliftmolem2  35425  cvmlift2lem11  35456  cvmliftphtlem  35460  mclsax  35712  weiunfr  36610  fin2so  37747  poimirlem18  37778  poimirlem21  37781  mblfinlem2  37798  itgabsnc  37829  itggt0cn  37830  prdsbnd  37933  prdstotbnd  37934  prdsbnd2  37935  rrnequiv  37975  eqlkr3  39300  dih1dimatlem  41528  3factsumint  42218  aks6d1c5lem2  42331  fnwe2lem1  43234  cantnf2  43509  nadd1suc  43576  imo72b2  44355  rfcnnnub  45223  disjxp1  45256  disjinfi  45378  fvixp2  45385  dmrelrnrel  45412  fvmptelcdmf  45456  suplesup  45526  infxr  45553  monoord2xrv  45669  climinf  45794  climsuse  45796  mullimc  45804  limccog  45808  mullimcf  45811  limcperiod  45816  limcleqr  45830  neglimc  45833  0ellimcdiv  45835  limclner  45837  limsuppnfdlem  45887  limsupubuzlem  45898  xlimmnfvlem2  46019  xlimpnfvlem2  46023  climxlim2lem  46031  dvdivbd  46109  ioodvbdlimc1lem1  46117  dvnprodlem2  46133  iblsplit  46152  stoweidlem5  46191  stoweidlem16  46202  stoweidlem21  46207  stoweidlem24  46210  stoweidlem25  46211  stoweidlem28  46214  stoweidlem31  46217  stoweidlem41  46227  stoweidlem42  46228  stoweidlem44  46230  stoweidlem45  46231  stoweidlem48  46234  stoweidlem51  46237  stoweidlem54  46240  stoweidlem57  46243  stoweidlem60  46246  stoweidlem62  46248  stirlinglem5  46264  dirkercncflem3  46291  fourierdlem11  46304  fourierdlem12  46305  fourierdlem14  46307  fourierdlem15  46308  fourierdlem31  46324  fourierdlem34  46327  fourierdlem41  46334  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem54  46346  fourierdlem69  46361  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem79  46371  fourierdlem80  46372  fourierdlem81  46373  fourierdlem92  46384  fourierdlem93  46385  fourierdlem94  46386  fourierdlem97  46389  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fourierdlem113  46405  etransclem32  46452  subsaliuncllem  46543  sge0rpcpnf  46607  caragendifcl  46700  iinhoiicclem  46859  pimdecfgtioc  46901  issmfgtlem  46941  ormklocald  47060  ormkglobd  47061  initopropd  49430  termopropd  49431  thincciso2  49642