Theorem ralimdva 3144

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		ralimdva.1	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 413	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 3143	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2081  ∀wral 3105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3110

This theorem is referenced by:  ralimdv  3145  ralimdvva  3146  wereu2  5440  fveqressseq  6712  f1mpt  6884  isores3  6951  caofrss  7300  caoftrn  7302  sorpssuni  7316  sorpssint  7317  onint  7366  smogt  7856  fisupg  8612  ixpfi2  8668  fissuni  8675  indexfi  8678  fiinfg  8809  wemaplem2  8857  rankonidlem  9103  ac5num  9308  acni2  9318  acndom2  9326  alephle  9360  dfac5  9400  cfsmolem  9538  isf34lem7  9647  isf34lem6  9648  fin1a2s  9682  acncc  9708  ttukeylem6  9782  fpwwe2lem8  9905  gchina  9967  inar1  10043  tskord  10048  grudomon  10085  grur1a  10087  dedekind  10650  fimaxre  11432  fimaxreOLD  11433  fiminre  11436  uzwo  12160  xrsupsslem  12550  xrinfmsslem  12551  fsuppmapnn0fiub0  13211  rexanre  14540  rexuz3  14542  rexico  14547  cau3lem  14548  limsupval2  14671  rlim2lt  14688  rlim3  14689  lo1bdd2  14715  lo1bddrp  14716  o1lo1  14728  climrlim2  14738  2clim  14763  o1co  14777  rlimcn1  14779  rlimcn2  14781  climcn1  14782  climcn2  14783  subcn2  14785  o1of2  14803  rlimo1  14807  o1rlimmul  14809  lo1add  14817  lo1mul  14818  climsqz  14831  climsqz2  14832  rlimsqzlem  14839  lo1le  14842  climbdd  14862  caucvgrlem  14863  caucvgrlem2  14865  caurcvg2  14868  iseralt  14875  cvgcmp  15004  cvgcmpce  15006  gcdcllem1  15681  absproddvds  15790  coprmprod  15834  coprmproddvdslem  15835  pcfac  16064  pockthg  16071  infpnlem1  16075  prmreclem2  16082  prmreclem3  16083  vdwlem11  16156  vdwlem13  16158  vdwnnlem3  16162  isacs2  16753  acsfn1  16761  acsfn2  16763  catpropd  16808  drsdirfi  17377  ipodrsima  17604  isacs5  17611  mrelatglb  17623  mrelatlub  17625  isgrpinv  17913  dfgrp3e  17956  issubg4  18052  gsmsymgreqlem2  18290  gexdvds  18439  gexcl3  18442  sylow2blem3  18477  cyggeninv  18725  gsummptnn0fz  18823  dprdff  18851  issubdrg  19250  acsfn1p  19268  mptcoe1fsupp  20066  cply1coe0bi  20151  gsummoncoe1  20155  cygznlem3  20398  scmatdmat  20808  mdetdiagid  20893  mdetunilem9  20913  cpmatmcllem  21010  m2cpminvid2lem  21046  decpmatmulsumfsupp  21065  pmatcollpw1lem1  21066  pmatcollpw2lem  21069  pmatcollpwfi  21074  pm2mpf1  21091  mptcoe1matfsupp  21094  mp2pm2mplem4  21101  pm2mpmhmlem1  21110  pm2mp  21117  chpdmat  21133  chpscmat  21134  cpmidpmatlem3  21164  cayhamlem4  21180  neiptopnei  21424  cncnp  21572  isnrm2  21650  isreg2  21669  2ndcdisj  21748  islly2  21776  dislly  21789  kgen2ss  21847  ptbasfi  21873  ptclsg  21907  prdstopn  21920  txtube  21932  txlm  21940  isr0  22029  filuni  22177  alexsubALTlem3  22341  ptcmplem3  22346  ptcmplem4  22347  tsmsxplem1  22444  prdsmet  22663  metequiv2  22803  metcnpi3  22839  nmoleub  23023  rescncf  23188  cncfco  23198  evth  23246  lebnumlem3  23250  xlebnum  23252  nmoleub2lem2  23403  nmhmcn  23407  lmmcvg  23547  cmetcaulem  23574  caubl  23594  bcth3  23617  ovollb2lem  23772  ovoliunlem2  23787  ovolicc2lem3  23803  ovolicc2lem4  23804  nulmbl2  23820  volsup  23840  ioombl1lem4  23845  dyadmax  23882  vitalilem2  23893  vitalilem5  23896  mbfi1flimlem  24006  itg2seq  24026  itg2addlem  24042  itgcn  24126  limciun  24175  rolle  24270  dvfsumrlim  24311  itgsubst  24329  aannenlem1  24600  aalioulem3  24606  ulmcaulem  24665  ulmcau  24666  ulmss  24668  ulmbdd  24669  ulmcn  24670  ulmdvlem3  24673  mtest  24675  iblulm  24678  itgulm  24679  rlimcnp  25225  xrlimcnp  25228  rlimcxp  25233  o1cxp  25234  amgm  25250  lgambdd  25296  ftalem2  25333  isppw2  25374  mumullem2  25439  2sqlem6  25681  chtppilimlem2  25732  chtppilim  25733  pntrsumbnd2  25825  pntlem3  25867  isperp2  26183  axeuclidlem  26431  axeuclid  26432  uhgrnbgr0nb  26819  vtxdginducedm1fi  27009  cusgrrusgr  27046  rusgrpropnb  27048  rusgrpropedg  27049  rusgrpropadjvtx  27050  upgrewlkle2  27071  wlkvtxiedg  27089  upgrwlkvtxedg  27109  uspgr2wlkeq  27110  redwlk  27139  wlkdlem2  27150  lfgrwlkprop  27154  2pthnloop  27199  upgr2pthnlp  27200  pthdlem1  27234  pthdlem2lem  27235  wlkiswwlks1  27332  wlkiswwlks2lem4  27337  wwlksm1edg  27346  wwlksnred  27357  clwwlkccatlem  27454  clwlkclwwlklem2a  27463  clwlkclwwlklem2  27465  cusconngr  27657  eucrctshift  27710  2pthfrgr  27755  3cyclfrgr  27759  nmoub3i  28241  ubthlem1  28338  ubthlem3  28340  ocsh  28751  chintcli  28799  chscllem2  29106  nmopub2tALT  29377  nmfnleub2  29394  lnconi  29501  riesz1  29533  rnbra  29575  leopadd  29600  leopmuli  29601  leoptr  29605  dmdbr3  29773  dmdbr4  29774  dmdbr5  29776  mdsl0  29778  mdsymlem6  29876  cdj1i  29901  acunirnmpt  30094  xrge0infss  30172  cmppcmp  30739  lmxrge0  30812  ftc2re  31486  cvmlift2lem12  32170  frpomin  32688  nosupbnd1lem5  32822  noetalem3  32829  opnrebl2  33279  neibastop1  33317  neibastop2lem  33318  neibastop3  33320  finixpnum  34427  lindsenlbs  34437  matunitlindflem1  34438  matunitlindflem2  34439  ptrecube  34442  poimirlem26  34468  poimirlem27  34469  poimirlem29  34471  poimirlem30  34472  poimir  34475  heicant  34477  itg2addnclem  34493  itg2addnclem3  34495  itg2addnc  34496  filbcmb  34566  nninfnub  34577  geomcau  34585  sstotbnd2  34603  isbndx  34611  prdsbnd  34622  heibor1lem  34638  heiborlem1  34640  heibor  34650  rrncmslem  34661  intidl  34858  pclclN  36577  lauteq  36781  ltrnid  36821  mapdh9a  38475  elrfirn2  38797  isnacs3  38811  rencldnfilem  38921  kelac1  39167  neik0pk1imk0  39901  cvgdvgrat  40202  neglimc  41489  limsupub  41546  limsuppnflem  41552  limsupre3lem  41574  limsupvaluz2  41580  supcnvlimsup  41582  climuzlem  41585  liminfval2  41610  limsupgtlem  41619  liminflelimsupuz  41627  liminflimsupclim  41649  xlimpnfxnegmnf  41656  liminflimsupxrre  41659  xlimmnfv  41676  xlimpnfv  41680  stoweidlem7  41854  fourierdlem73  42026  sge0isum  42271  meaiuninc3v  42328  preimageiingt  42560  preimaleiinlt  42561  smflimlem3  42611  smflimlem4  42612  2reu8i  42848  iccpartres  43080  upwlkwlk  43516  upgrwlkupwlk  43517  copisnmnd  43578  2zrngnmlid2  43720  ply1mulgsumlem1  43940  ply1mulgsumlem3  43942  ply1mulgsumlem4  43943  snlindsntor  44026  eenglngeehlnmlem1  44225  eenglngeehlnmlem2  44226