Theorem r19.21bi 3234

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3052

This theorem is referenced by:  r19.21be  3235  rspec2  3261  rspec3  3262  ralxfr2d  5380  fvmptelcdm  7102  fompt  7107  f1oresrab  7116  isoselem  7333  mpoexw  8075  naddsuc2  8711  boxcutc  8953  xpf1o  9151  fineqvlem  9268  indexfi  9370  dffi3  9441  suppr  9482  supiso  9486  infpr  9515  ordtypelem9  9538  brwdom3  9594  xpwdomg  9597  ixpiunwdom  9602  infxpenc2lem1  10031  hsmexlem4  10441  gchina  10711  wunom  10732  prcdnq  11005  prnmax  11007  dedekind  11396  dedekindle  11397  monoord2  14049  limsupgre  15495  limsupbnd1  15496  limsupbnd2  15497  climmpt2  15587  rlimcld2  15592  climsup  15684  sumpr  15762  sumtp  15763  fsum2dlem  15784  fsumiun  15835  fprod2dlem  15994  iserodd  16853  vdwlem1  16999  vdwlem6  17004  vdwnnlem3  17015  imasvscafn  17549  fuciso  17989  evlfcl  18232  yonedainv  18291  oduprs  18310  acsmapd  18562  prdsmndd  18746  psgnunilem5  19473  gsummpt1n0  19944  dprdspan  20008  ablfaclem2  20067  srgdilem  20150  srgrz  20165  srglz  20166  issrngd  20813  frgpcyg  21532  psrbaglesupp  21880  psrbagcon  21883  psrbagleadd1  21886  evlslem2  22035  mpfind  22063  psdmul  22102  ply1chr  22242  gsumsmonply1  22243  gsummoncoe1  22244  evl1gsummon  22301  cpmatmcllem  22654  neiptoptop  23067  neiptopnei  23068  ordtrest2lem  23139  cncmp  23328  1stckgenlem  23489  ptcld  23549  dfac14  23554  ptcnplem  23557  pthaus  23574  xkococnlem  23595  xkococn  23596  cnmpt2k  23624  xpstopnlem1  23745  cnpflfi  23935  ptcmplem2  23989  cnextcn  24003  cnextfres1  24004  cnmpt2plusg  24024  cnmpt2vsca  24131  ustfilxp  24149  utoptop  24171  restutop  24174  restutopopn  24175  ucncn  24221  cfilufg  24229  trcfilu  24230  psmet0  24245  psmettri2  24246  prdsxmetlem  24305  prdsbl  24428  prdsxmslem2  24466  psmetutop  24504  cnmpt2ds  24781  bndth  24906  cnmpt2ip  25198  iscmet3lem2  25242  cmetcusp1  25303  rrxcph  25342  ovoliunlem1  25453  ovoliunlem3  25455  ovoliun  25456  ovoliun2  25457  ovolscalem1  25464  volfiniun  25498  uniioombllem4  25537  mbfeqalem1  25592  mbfres2  25596  ismbf3d  25605  mbfsup  25615  mbfinf  25616  mbflim  25619  itg1ge0  25637  itg1mulc  25655  itg1climres  25665  mbfi1fseqlem4  25669  itg2lea  25695  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2mono  25704  itg2i1fseqle  25705  itg2i1fseq  25706  itg2addlem  25709  itg2cnlem1  25712  itgeqa  25765  itgfsum  25778  itgabs  25786  itggt0  25795  dvlipcn  25949  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  coeeulem  26179  dgrlem  26184  dgrlb  26191  coeaddlem  26204  coecj  26234  coecjOLD  26236  ulmss  26356  leibpi  26902  xrlimcnp  26928  o1cxp  26935  jensen  26949  lgambdd  26997  wilthlem2  27029  sqff1o  27142  fsumdvdscom  27145  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  dchrmulcl  27210  dchrmullid  27213  dchrinv  27222  dchrvmasumlem2  27459  ostth1  27594  conway  27761  slerec  27781  ercgrg  28442  f1otrg  28796  f1otrge  28797  ubthlem2  30798  fmptcof2  32581  disjdsct  32626  fprodex01  32750  prodindf  32786  ccatf1  32870  ressprs  32890  mgcf1o  32929  chnccats1  32941  gsumpart  32997  archiabl  33142  lmodslmd  33147  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnsubrunlem2  33189  rhmimaidl  33393  gsummoncoe1fzo  33553  ply1gsumz  33554  fedgmullem2  33616  fedgmul  33617  txomap  33811  qtophaus  33813  locfinreflem  33817  ordtrest2NEWlem  33899  lmdvg  33930  zrhcntr  33956  esumcl  34007  esumeq2d  34014  esumnul  34025  hasheuni  34062  esumcvg  34063  esumcvgre  34068  insiga  34114  ldsysgenld  34137  ldgenpisyslem1  34140  measvunilem  34189  measvunilem0  34190  measdivcstALTV  34202  cntmeas  34203  voliune  34206  volfiniune  34207  1stmbfm  34238  2ndmbfm  34239  omssubadd  34278  difelcarsg  34288  inelcarsg  34289  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemgvv  34354  dstrvprob  34450  hashreprin  34598  reprgt  34599  breprexplemc  34610  circlemeth  34618  hgt750lema  34635  tgoldbachgtd  34640  bnj93  34840  bnj518  34863  bnj1489  35033  fnrelpredd  35066  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  ptpconn  35201  resconn  35214  cvmliftmolem2  35250  cvmlift2lem11  35281  cvmliftphtlem  35285  mclsax  35537  weiunfr  36431  fin2so  37577  poimirlem18  37608  poimirlem21  37611  mblfinlem2  37628  itgabsnc  37659  itggt0cn  37660  prdsbnd  37763  prdstotbnd  37764  prdsbnd2  37765  rrnequiv  37805  eqlkr3  39065  dih1dimatlem  41294  3factsumint  41984  aks6d1c5lem2  42097  fnwe2lem1  43021  cantnf2  43296  nadd1suc  43363  imo72b2  44143  rfcnnnub  45008  disjxp1  45041  disjinfi  45164  fvixp2  45171  dmrelrnrel  45198  fvmptelcdmf  45242  suplesup  45314  infxr  45342  monoord2xrv  45458  climinf  45583  climsuse  45585  mullimc  45593  limccog  45597  mullimcf  45600  limcperiod  45605  limcleqr  45621  neglimc  45624  0ellimcdiv  45626  limclner  45628  limsuppnfdlem  45678  limsupubuzlem  45689  xlimmnfvlem2  45810  xlimpnfvlem2  45814  climxlim2lem  45822  dvdivbd  45900  ioodvbdlimc1lem1  45908  dvnprodlem2  45924  iblsplit  45943  stoweidlem5  45982  stoweidlem16  45993  stoweidlem21  45998  stoweidlem24  46001  stoweidlem25  46002  stoweidlem28  46005  stoweidlem31  46008  stoweidlem41  46018  stoweidlem42  46019  stoweidlem44  46021  stoweidlem45  46022  stoweidlem48  46025  stoweidlem51  46028  stoweidlem54  46031  stoweidlem57  46034  stoweidlem60  46037  stoweidlem62  46039  stirlinglem5  46055  dirkercncflem3  46082  fourierdlem11  46095  fourierdlem12  46096  fourierdlem14  46098  fourierdlem15  46099  fourierdlem31  46115  fourierdlem34  46118  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem54  46137  fourierdlem69  46152  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem79  46162  fourierdlem80  46163  fourierdlem81  46164  fourierdlem92  46175  fourierdlem93  46176  fourierdlem94  46177  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem113  46196  etransclem32  46243  subsaliuncllem  46334  sge0rpcpnf  46398  caragendifcl  46491  iinhoiicclem  46650  pimdecfgtioc  46692  issmfgtlem  46732  ormklocald  46851  ormkglobd  46852  initopropd  49108  termopropd  49109  thincciso2  49289