Theorem r19.21bi 3224

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 3221	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜓 ∧ 𝑥 ∈ 𝐴) → 𝜓)
3	1, 2	sylan 580	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

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 2180

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

This theorem is referenced by:  r19.21be  3225  rspec2  3251  rspec3  3252  ralxfr2d  5346  fvmptelcdm  7046  fompt  7051  f1oresrab  7060  isoselem  7275  mpoexw  8010  naddsuc2  8616  boxcutc  8865  xpf1o  9052  fineqvlem  9150  indexfi  9244  dffi3  9315  suppr  9356  supiso  9360  infpr  9389  ordtypelem9  9412  brwdom3  9468  xpwdomg  9471  ixpiunwdom  9476  infxpenc2lem1  9910  hsmexlem4  10320  gchina  10590  wunom  10611  prcdnq  10884  prnmax  10886  dedekind  11276  dedekindle  11277  monoord2  13940  limsupgre  15388  limsupbnd1  15389  limsupbnd2  15390  climmpt2  15480  rlimcld2  15485  climsup  15577  sumpr  15655  sumtp  15656  fsum2dlem  15677  fsumiun  15728  fprod2dlem  15887  iserodd  16747  vdwlem1  16893  vdwlem6  16898  vdwnnlem3  16909  imasvscafn  17441  fuciso  17885  evlfcl  18128  yonedainv  18187  oduprs  18206  acsmapd  18460  chnccats1  18531  chnccat  18532  prdsmndd  18678  psgnunilem5  19406  gsummpt1n0  19877  dprdspan  19941  ablfaclem2  20000  srgdilem  20110  srgrz  20125  srglz  20126  issrngd  20770  frgpcyg  21510  psrbaglesupp  21859  psrbagcon  21862  psrbagleadd1  21865  evlslem2  22014  mpfind  22042  psdmul  22081  ply1chr  22221  gsumsmonply1  22222  gsummoncoe1  22223  evl1gsummon  22280  cpmatmcllem  22633  neiptoptop  23046  neiptopnei  23047  ordtrest2lem  23118  cncmp  23307  1stckgenlem  23468  ptcld  23528  dfac14  23533  ptcnplem  23536  pthaus  23553  xkococnlem  23574  xkococn  23575  cnmpt2k  23603  xpstopnlem1  23724  cnpflfi  23914  ptcmplem2  23968  cnextcn  23982  cnextfres1  23983  cnmpt2plusg  24003  cnmpt2vsca  24110  ustfilxp  24128  utoptop  24149  restutop  24152  restutopopn  24153  ucncn  24199  cfilufg  24207  trcfilu  24208  psmet0  24223  psmettri2  24224  prdsxmetlem  24283  prdsbl  24406  prdsxmslem2  24444  psmetutop  24482  cnmpt2ds  24759  bndth  24884  cnmpt2ip  25175  iscmet3lem2  25219  cmetcusp1  25280  rrxcph  25319  ovoliunlem1  25430  ovoliunlem3  25432  ovoliun  25433  ovoliun2  25434  ovolscalem1  25441  volfiniun  25475  uniioombllem4  25514  mbfeqalem1  25569  mbfres2  25573  ismbf3d  25582  mbfsup  25592  mbfinf  25593  mbflim  25596  itg1ge0  25614  itg1mulc  25632  itg1climres  25642  mbfi1fseqlem4  25646  itg2lea  25672  itg2splitlem  25676  itg2split  25677  itg2monolem1  25678  itg2mono  25681  itg2i1fseqle  25682  itg2i1fseq  25683  itg2addlem  25686  itg2cnlem1  25689  itgeqa  25742  itgfsum  25755  itgabs  25763  itggt0  25772  dvlipcn  25926  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  itgsubstlem  25982  coeeulem  26156  dgrlem  26161  dgrlb  26168  coeaddlem  26181  coecj  26211  coecjOLD  26213  ulmss  26333  leibpi  26879  xrlimcnp  26905  o1cxp  26912  jensen  26926  lgambdd  26974  wilthlem2  27006  sqff1o  27119  fsumdvdscom  27122  fsumdvdsmul  27132  fsumdvdsmulOLD  27134  dchrmulcl  27187  dchrmullid  27190  dchrinv  27199  dchrvmasumlem2  27436  ostth1  27571  conway  27740  slerec  27760  ercgrg  28495  f1otrg  28849  f1otrge  28850  ubthlem2  30851  fmptcof2  32639  disjdsct  32684  fprodex01  32808  prodindf  32844  ccatf1  32930  ressprs  32947  mgcf1o  32984  gsumpart  33037  archiabl  33167  lmodslmd  33173  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnsubrunlem2  33215  rhmimaidl  33397  gsummoncoe1fzo  33558  ply1gsumz  33559  fedgmullem2  33643  fedgmul  33644  txomap  33847  qtophaus  33849  locfinreflem  33853  ordtrest2NEWlem  33935  lmdvg  33966  zrhcntr  33992  esumcl  34043  esumeq2d  34050  esumnul  34061  hasheuni  34098  esumcvg  34099  esumcvgre  34104  insiga  34150  ldsysgenld  34173  ldgenpisyslem1  34176  measvunilem  34225  measvunilem0  34226  measdivcstALTV  34238  cntmeas  34239  voliune  34242  volfiniune  34243  1stmbfm  34273  2ndmbfm  34274  omssubadd  34313  difelcarsg  34323  inelcarsg  34324  eulerpartlems  34373  eulerpartlemsv3  34374  eulerpartlemgvv  34389  dstrvprob  34485  hashreprin  34633  reprgt  34634  breprexplemc  34645  circlemeth  34653  hgt750lema  34670  tgoldbachgtd  34675  bnj93  34875  bnj518  34898  bnj1489  35068  fnrelpredd  35102  subfacp1lem3  35226  subfacp1lem5  35228  erdszelem8  35242  ptpconn  35277  resconn  35290  cvmliftmolem2  35326  cvmlift2lem11  35357  cvmliftphtlem  35361  mclsax  35613  weiunfr  36509  fin2so  37655  poimirlem18  37686  poimirlem21  37689  mblfinlem2  37706  itgabsnc  37737  itggt0cn  37738  prdsbnd  37841  prdstotbnd  37842  prdsbnd2  37843  rrnequiv  37883  eqlkr3  39148  dih1dimatlem  41376  3factsumint  42066  aks6d1c5lem2  42179  fnwe2lem1  43091  cantnf2  43366  nadd1suc  43433  imo72b2  44213  rfcnnnub  45081  disjxp1  45114  disjinfi  45237  fvixp2  45244  dmrelrnrel  45271  fvmptelcdmf  45315  suplesup  45386  infxr  45413  monoord2xrv  45529  climinf  45654  climsuse  45656  mullimc  45664  limccog  45668  mullimcf  45671  limcperiod  45676  limcleqr  45690  neglimc  45693  0ellimcdiv  45695  limclner  45697  limsuppnfdlem  45747  limsupubuzlem  45758  xlimmnfvlem2  45879  xlimpnfvlem2  45883  climxlim2lem  45891  dvdivbd  45969  ioodvbdlimc1lem1  45977  dvnprodlem2  45993  iblsplit  46012  stoweidlem5  46051  stoweidlem16  46062  stoweidlem21  46067  stoweidlem24  46070  stoweidlem25  46071  stoweidlem28  46074  stoweidlem31  46077  stoweidlem41  46087  stoweidlem42  46088  stoweidlem44  46090  stoweidlem45  46091  stoweidlem48  46094  stoweidlem51  46097  stoweidlem54  46100  stoweidlem57  46103  stoweidlem60  46106  stoweidlem62  46108  stirlinglem5  46124  dirkercncflem3  46151  fourierdlem11  46164  fourierdlem12  46165  fourierdlem14  46167  fourierdlem15  46168  fourierdlem31  46184  fourierdlem34  46187  fourierdlem41  46194  fourierdlem48  46200  fourierdlem49  46201  fourierdlem50  46202  fourierdlem54  46206  fourierdlem69  46221  fourierdlem73  46225  fourierdlem74  46226  fourierdlem75  46227  fourierdlem76  46228  fourierdlem79  46231  fourierdlem80  46232  fourierdlem81  46233  fourierdlem92  46244  fourierdlem93  46245  fourierdlem94  46246  fourierdlem97  46249  fourierdlem103  46255  fourierdlem104  46256  fourierdlem111  46263  fourierdlem113  46265  etransclem32  46312  subsaliuncllem  46403  sge0rpcpnf  46467  caragendifcl  46560  iinhoiicclem  46719  pimdecfgtioc  46761  issmfgtlem  46801  ormklocald  46920  ormkglobd  46921  initopropd  49283  termopropd  49284  thincciso2  49495