Theorem ralimdva 3177

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 417	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 30	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 3174	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is referenced by:  ralimdv  3179  ralimdvva  3212  wereu2  5658  frpomin  6341  fveqressseq  7074  f1mpt  7259  isores3  7333  caofrss  7713  caoftrn  7715  sorpssuni  7729  sorpssint  7730  onint  7785  xpord3inddlem  8146  smogt  8350  fisupg  9244  ixpfi2  9303  fissuni  9310  indexfi  9313  fiinfg  9457  wemaplem2  9505  rankonidlem  9796  ac5num  10016  acni2  10026  acndom2  10034  alephle  10068  dfac5  10108  cfsmolem  10249  isf34lem7  10358  isf34lem6  10359  fin1a2s  10393  acncc  10419  ttukeylem6  10493  fpwwe2lem7  10617  gchina  10679  inar1  10755  tskord  10760  grudomon  10797  grur1a  10799  dedekind  11368  fimaxre  12154  fiminre  12157  uzwo  12930  xrsupsslem  13328  xrinfmsslem  13329  fsuppmapnn0fiub0  14025  rexanre  15394  rexuz3  15396  rexico  15401  cau3lem  15402  limsupval2  15527  rlim2lt  15544  rlim3  15545  lo1bdd2  15571  lo1bddrp  15572  o1lo1  15584  climrlim2  15594  2clim  15619  o1co  15633  rlimcn1  15635  rlimcn3  15637  climcn1  15639  climcn2  15640  subcn2  15642  o1of2  15660  rlimo1  15664  o1rlimmul  15666  lo1add  15674  lo1mul  15675  climsqz  15688  climsqz2  15689  rlimsqzlem  15696  lo1le  15699  climbdd  15719  caucvgrlem  15720  caucvgrlem2  15722  caurcvg2  15725  iseralt  15732  cvgcmp  15864  cvgcmpce  15866  gcdcllem1  16552  absproddvds  16670  coprmprod  16714  coprmproddvdslem  16715  pcfac  16954  pockthg  16961  infpnlem1  16965  prmreclem2  16972  prmreclem3  16973  vdwlem11  17046  vdwlem13  17048  vdwnnlem3  17052  isacs2  17704  acsfn1  17712  acsfn2  17714  catpropd  17760  drsdirfi  18356  ipodrsima  18592  isacs5  18599  mrelatglb  18611  mrelatlub  18613  isgrpinv  19055  dfgrp3e  19101  issubg4  19207  gsmsymgreqlem2  19496  finodsubmsubg  19632  gexdvds  19649  gexcl3  19652  sylow2blem3  19687  cyggeninv  19948  gsummptnn0fz  20051  dprdff  20079  isdrng4  20839  issubdrg  20883  acsfn1p  20902  cygznlem3  21719  psdmul  22329  mptcoe1fsupp  22375  cply1coe0bi  22462  gsummoncoe1  22468  evls1fpws  22529  scmatdmat  22672  mdetdiagid  22757  mdetunilem9  22777  cpmatmcllem  22875  m2cpminvid2lem  22911  decpmatmulsumfsupp  22930  pmatcollpw1lem1  22931  pmatcollpw2lem  22934  pmatcollpwfi  22939  pm2mpf1  22956  mptcoe1matfsupp  22959  mp2pm2mplem4  22966  pm2mpmhmlem1  22975  pm2mp  22982  chpdmat  22998  chpscmat  22999  cpmidpmatlem3  23029  cayhamlem4  23045  neiptopnei  23289  cncnp  23437  isnrm2  23515  isreg2  23534  2ndcdisj  23613  islly2  23641  dislly  23654  kgen2ss  23712  ptbasfi  23738  ptclsg  23772  prdstopn  23785  txtube  23797  txlm  23805  isr0  23894  filuni  24042  alexsubALTlem3  24206  ptcmplem3  24211  ptcmplem4  24212  tsmsxplem1  24310  prdsmet  24527  metequiv2  24667  metcnpi3  24703  nmoleub  24888  rescncf  25056  cncfco  25066  evth  25118  lebnumlem3  25122  xlebnum  25124  nmoleub2lem2  25275  nmhmcn  25279  lmmcvg  25420  cmetcaulem  25447  caubl  25467  bcth3  25490  ovollb2lem  25647  ovoliunlem2  25662  ovolicc2lem3  25678  ovolicc2lem4  25679  nulmbl2  25695  volsup  25715  ioombl1lem4  25720  dyadmax  25757  vitalilem2  25768  vitalilem5  25771  mbfi1flimlem  25881  itg2seq  25901  itg2addlem  25917  itgcn  26004  limciun  26053  rolle  26149  dvfsumrlim  26190  itgsubst  26208  aannenlem1  26491  aalioulem3  26497  ulmcaulem  26557  ulmcau  26558  ulmss  26560  ulmbdd  26561  ulmcn  26562  ulmdvlem3  26565  mtest  26567  iblulm  26570  itgulm  26571  rlimcnp  27130  xrlimcnp  27133  rlimcxp  27138  o1cxp  27139  amgm  27155  lgambdd  27201  ftalem2  27238  isppw2  27279  mumullem2  27344  2sqlem6  27587  chtppilimlem2  27638  chtppilim  27639  pntrsumbnd2  27731  pntlem3  27773  nosupbnd1lem5  27876  noinfbnd1lem5  27891  noetasuplem4  27900  noetainflem4  27904  negbdaylem  28249  mulsuniflem  28342  elreno2  28688  isperp2  28995  axeuclidlem  29312  axeuclid  29313  uhgrnbgr0nb  29704  vtxdginducedm1fi  29894  cusgrrusgr  29931  rusgrpropnb  29933  rusgrpropedg  29934  rusgrpropadjvtx  29935  upgrewlkle2  29956  wlkvtxiedg  29974  upgrwlkvtxedg  29994  uspgr2wlkeq  29995  redwlk  30020  wlkdlem2  30031  lfgrwlkprop  30035  2pthnloop  30080  upgr2pthnlp  30081  pthdlem1  30115  pthdlem2lem  30116  wlkiswwlks1  30216  wlkiswwlks2lem4  30221  wwlksm1edg  30230  wwlksnred  30241  clwwlkccatlem  30340  clwlkclwwlklem2a  30349  clwlkclwwlklem2  30351  cusconngr  30542  eucrctshift  30594  2pthfrgr  30635  3cyclfrgr  30639  nmoub3i  31125  ubthlem1  31222  ubthlem3  31224  ocsh  31635  chintcli  31683  chscllem2  31990  nmopub2tALT  32261  nmfnleub2  32278  lnconi  32385  riesz1  32417  rnbra  32459  leopadd  32484  leopmuli  32485  leoptr  32489  dmdbr3  32657  dmdbr4  32658  dmdbr5  32660  mdsl0  32662  mdsymlem6  32760  cdj1i  32785  acunirnmpt  33004  xrge0infss  33105  elrspunidl  33736  dflring2  33783  cmppcmp  34248  zarclsiin  34261  lmxrge0  34342  ftc2re  34985  cvmlift2lem12  35806  nmulrid  36689  opnrebl2  36852  neibastop1  36890  neibastop2lem  36891  neibastop3  36893  finixpnum  38276  lindsenlbs  38286  matunitlindflem1  38287  matunitlindflem2  38288  ptrecube  38291  poimirlem26  38317  poimirlem27  38318  poimirlem29  38320  poimirlem30  38321  poimir  38324  heicant  38326  itg2addnclem  38342  itg2addnclem3  38344  itg2addnc  38345  filbcmb  38411  nninfnub  38422  geomcau  38430  sstotbnd2  38445  isbndx  38453  prdsbnd  38464  heibor1lem  38480  heiborlem1  38482  heibor  38492  rrncmslem  38503  intidl  38700  pclclN  40685  lauteq  40889  ltrnid  40929  mapdh9a  42583  primrootscoprmpow  42886  sticksstones3  42935  aks5lem5a  42978  aks5lem6  42979  fltaccoprm  43392  fltabcoprm  43394  flt4lem5  43402  elrfirn2  43447  isnacs3  43461  rencldnfilem  43567  kelac1  43810  naddgeoa  44141  neik0pk1imk0  44793  cvgdvgrat  45043  neglimc  46381  limsupub  46438  limsuppnflem  46444  limsupre3lem  46466  limsupvaluz2  46472  supcnvlimsup  46474  climuzlem  46477  liminfval2  46502  limsupgtlem  46511  liminflelimsupuz  46519  liminflimsupclim  46541  xlimpnfxnegmnf  46548  liminflimsupxrre  46551  xlimmnfv  46568  xlimpnfv  46572  stoweidlem7  46741  fourierdlem73  46913  sge0isum  47161  meaiuninc3v  47218  preimageiingt  47454  preimaleiinlt  47455  smflimlem3  47507  smflimlem4  47508  cfsetsnfsetfo  47817  2reu8i  47870  iccpartres  48187  uhgrimisgrgric  48716  grlictr  48800  clnbgr3stgrgrlim  48804  clnbgr3stgrgrlic  48805  upwlkwlk  48924  upgrwlkupwlk  48925  copisnmnd  48954  2zrngnmlid2  49042  ply1mulgsumlem1  49186  ply1mulgsumlem3  49188  ply1mulgsumlem4  49189  snlindsntor  49271  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  iinfsubc  49856