Theorem r19.21bi 3263

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086

This theorem is referenced by:  r19.21be  3264  rspec2  3290  rspec3  3291  ralxfr2d  5382  fvmptelcdm  7109  fompt  7114  f1oresrab  7124  isoselem  7340  mpoexw  8074  naddsuc2  8687  boxcutc  8938  xpf1o  9126  fineqvlem  9225  indexfi  9316  dffi3  9390  suppr  9431  supiso  9435  infpr  9464  ordtypelem9  9487  brwdom3  9543  xpwdomg  9546  ixpiunwdom  9551  infxpenc2lem1  10002  hsmexlem4  10412  gchina  10683  wunom  10704  prcdnq  10977  prnmax  10979  dedekind  11372  dedekindle  11373  monoord2  14068  limsupgre  15531  limsupbnd1  15532  limsupbnd2  15533  climmpt2  15623  rlimcld2  15628  climsup  15720  sumpr  15798  sumtp  15799  fsum2dlem  15820  fsumiun  15872  fprod2dlem  16033  iserodd  16894  vdwlem1  17040  vdwlem6  17045  vdwnnlem3  17056  imasvscafn  17590  fuciso  18034  evlfcl  18277  yonedainv  18336  oduprs  18355  acsmapd  18609  chnccats1  18680  chnccat  18681  prdsmndd  18827  psgnunilem5  19563  gsummpt1n0  20034  dprdspan  20098  ablfaclem2  20157  srgdilem  20273  srgrz  20288  srglz  20289  issrngd  20935  frgpcyg  21691  psrbaglesupp  22040  psrbagcon  22043  psrbagleadd1  22046  evlslem2  22198  mpfind  22234  psdmul  22297  ply1chr  22434  gsumsmonply1  22435  gsummoncoe1  22436  evl1gsummon  22493  cpmatmcllem  22843  neiptoptop  23256  neiptopnei  23257  ordtrest2lem  23328  cncmp  23517  1stckgenlem  23678  ptcld  23738  dfac14  23743  ptcnplem  23746  pthaus  23763  xkococnlem  23784  xkococn  23785  cnmpt2k  23813  xpstopnlem1  23934  cnpflfi  24124  ptcmplem2  24178  cnextcn  24192  cnextfres1  24193  cnmpt2plusg  24213  cnmpt2vsca  24320  ustfilxp  24338  utoptop  24359  restutop  24362  restutopopn  24363  ucncn  24409  cfilufg  24417  trcfilu  24418  psmet0  24433  psmettri2  24434  prdsxmetlem  24493  prdsbl  24616  prdsxmslem2  24654  psmetutop  24692  cnmpt2ds  24969  bndth  25085  cnmpt2ip  25375  iscmet3lem2  25419  cmetcusp1  25480  rrxcph  25519  ovoliunlem1  25629  ovoliunlem3  25631  ovoliun  25632  ovoliun2  25633  ovolscalem1  25640  volfiniun  25674  uniioombllem4  25713  mbfeqalem1  25768  mbfres2  25772  ismbf3d  25781  mbfsup  25791  mbfinf  25792  mbflim  25795  itg1ge0  25813  itg1mulc  25831  itg1climres  25841  mbfi1fseqlem4  25845  itg2lea  25871  itg2splitlem  25875  itg2split  25876  itg2monolem1  25877  itg2mono  25880  itg2i1fseqle  25881  itg2i1fseq  25882  itg2addlem  25885  itg2cnlem1  25888  itgeqa  25941  itgfsum  25954  itgabs  25962  itggt0  25971  dvlipcn  26121  dvfsumabs  26150  dvfsumlem2  26154  itgsubstlem  26175  coeeulem  26349  dgrlem  26354  dgrlb  26361  coeaddlem  26374  coecj  26403  coecjOLD  26405  ulmss  26525  leibpi  27072  xrlimcnp  27098  o1cxp  27104  jensen  27118  lgambdd  27166  wilthlem2  27198  sqff1o  27311  fsumdvdscom  27314  fsumdvdsmul  27324  dchrmulcl  27378  dchrmullid  27381  dchrinv  27390  dchrvmasumlem2  27627  ostth1  27762  conway  27937  lesrec  27957  ercgrg  28751  f1otrg  29160  f1otrge  29161  ubthlem2  31163  fmptcof2  32942  disjdsct  32988  fprodex01  33109  prodindf  33122  ccatf1  33209  ressprs  33226  mgcf1o  33263  gsumpart  33323  suppgsumssiun  33332  archiabl  33458  lmodslmd  33464  elrgspnlem1  33502  elrgspnlem2  33503  elrgspnsubrunlem2  33508  rhmimaidl  33683  gsummoncoe1fzo  33831  ply1gsumz  33833  vietadeg1  33912  vietalem  33913  fedgmullem2  33964  fedgmul  33965  txomap  34168  qtophaus  34170  locfinreflem  34174  ordtrest2NEWlem  34256  lmdvg  34287  zrhcntr  34313  esumcl  34364  esumeq2d  34371  esumnul  34382  hasheuni  34419  esumcvg  34420  esumcvgre  34425  insiga  34471  ldsysgenld  34494  ldgenpisyslem1  34497  measvunilem  34546  measvunilem0  34547  measdivcstALTV  34559  cntmeas  34560  voliune  34563  volfiniune  34564  1stmbfm  34594  2ndmbfm  34595  omssubadd  34634  difelcarsg  34644  inelcarsg  34645  eulerpartlems  34694  eulerpartlemsv3  34695  eulerpartlemgvv  34710  dstrvprob  34806  hashreprin  34951  reprgt  34952  breprexplemc  34963  circlemeth  34971  hgt750lema  34988  tgoldbachgtd  34993  bnj93  35195  bnj518  35218  bnj1489  35388  fnrelpredd  35424  subfacp1lem3  35572  subfacp1lem5  35574  erdszelem8  35588  ptpconn  35623  resconn  35636  cvmliftmolem2  35672  cvmlift2lem11  35703  cvmliftphtlem  35707  mclsax  35959  weiunfr  36866  fin2so  38145  poimirlem18  38176  poimirlem21  38179  mblfinlem2  38196  itgabsnc  38227  itggt0cn  38228  prdsbnd  38331  prdstotbnd  38332  prdsbnd2  38333  rrnequiv  38373  eqlkr3  39764  dih1dimatlem  41992  3factsumint  42681  aks6d1c5lem2  42794  fnwe2lem1  43668  cantnf2  43943  nadd1suc  44010  imo72b2  44789  rfcnnnub  45647  disjxp1  45680  disjinfi  45801  fvixp2  45807  dmrelrnrel  45833  fvmptelcdmf  45876  suplesup  45946  infxr  45973  monoord2xrv  46088  climinf  46213  climsuse  46215  mullimc  46223  limccog  46227  mullimcf  46230  limcperiod  46235  limcleqr  46249  neglimc  46252  0ellimcdiv  46254  limclner  46256  limsuppnfdlem  46306  limsupubuzlem  46317  xlimmnfvlem2  46438  xlimpnfvlem2  46442  climxlim2lem  46450  dvdivbd  46528  ioodvbdlimc1lem1  46536  dvnprodlem2  46552  iblsplit  46571  stoweidlem5  46610  stoweidlem16  46621  stoweidlem21  46626  stoweidlem24  46629  stoweidlem25  46630  stoweidlem28  46633  stoweidlem31  46636  stoweidlem41  46646  stoweidlem42  46647  stoweidlem44  46649  stoweidlem45  46650  stoweidlem48  46653  stoweidlem51  46656  stoweidlem54  46659  stoweidlem57  46662  stoweidlem60  46665  stoweidlem62  46667  stirlinglem5  46683  dirkercncflem3  46710  fourierdlem11  46723  fourierdlem12  46724  fourierdlem14  46726  fourierdlem15  46727  fourierdlem31  46743  fourierdlem34  46746  fourierdlem41  46753  fourierdlem48  46759  fourierdlem49  46760  fourierdlem50  46761  fourierdlem54  46765  fourierdlem69  46780  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem79  46790  fourierdlem80  46791  fourierdlem81  46792  fourierdlem92  46803  fourierdlem93  46804  fourierdlem94  46805  fourierdlem97  46808  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fourierdlem113  46824  etransclem32  46871  subsaliuncllem  46962  sge0rpcpnf  47026  caragendifcl  47119  iinhoiicclem  47278  pimdecfgtioc  47320  issmfgtlem  47360  ormklocald  47481  ormkglobd  47482  initopropd  49905  termopropd  49906  thincciso2  50117