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 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 3141	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

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

This theorem is referenced by:  ralimdv  3146  ralimdvva  3179  wereu2  5611  frpomin  6287  fveqressseq  7012  f1mpt  7195  isores3  7269  caofrss  7649  caoftrn  7651  sorpssuni  7665  sorpssint  7666  onint  7723  xpord3inddlem  8084  smogt  8287  fisupg  9172  ixpfi2  9234  fissuni  9241  indexfi  9244  fiinfg  9385  wemaplem2  9433  rankonidlem  9721  ac5num  9927  acni2  9937  acndom2  9945  alephle  9979  dfac5  10020  cfsmolem  10161  isf34lem7  10270  isf34lem6  10271  fin1a2s  10305  acncc  10331  ttukeylem6  10405  fpwwe2lem7  10528  gchina  10590  inar1  10666  tskord  10671  grudomon  10708  grur1a  10710  dedekind  11276  fimaxre  12066  fiminre  12069  uzwo  12809  xrsupsslem  13206  xrinfmsslem  13207  fsuppmapnn0fiub0  13900  rexanre  15254  rexuz3  15256  rexico  15261  cau3lem  15262  limsupval2  15387  rlim2lt  15404  rlim3  15405  lo1bdd2  15431  lo1bddrp  15432  o1lo1  15444  climrlim2  15454  2clim  15479  o1co  15493  rlimcn1  15495  rlimcn3  15497  climcn1  15499  climcn2  15500  subcn2  15502  o1of2  15520  rlimo1  15524  o1rlimmul  15526  lo1add  15534  lo1mul  15535  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  lo1le  15559  climbdd  15579  caucvgrlem  15580  caucvgrlem2  15582  caurcvg2  15585  iseralt  15592  cvgcmp  15723  cvgcmpce  15725  gcdcllem1  16410  absproddvds  16528  coprmprod  16572  coprmproddvdslem  16573  pcfac  16811  pockthg  16818  infpnlem1  16822  prmreclem2  16829  prmreclem3  16830  vdwlem11  16903  vdwlem13  16905  vdwnnlem3  16909  isacs2  17559  acsfn1  17567  acsfn2  17569  catpropd  17615  drsdirfi  18211  ipodrsima  18447  isacs5  18454  mrelatglb  18466  mrelatlub  18468  isgrpinv  18906  dfgrp3e  18953  issubg4  19058  gsmsymgreqlem2  19343  finodsubmsubg  19479  gexdvds  19496  gexcl3  19499  sylow2blem3  19534  cyggeninv  19795  gsummptnn0fz  19898  dprdff  19926  issubdrg  20695  acsfn1p  20714  cygznlem3  21506  psdmul  22081  mptcoe1fsupp  22128  cply1coe0bi  22217  gsummoncoe1  22223  evls1fpws  22284  scmatdmat  22430  mdetdiagid  22515  mdetunilem9  22535  cpmatmcllem  22633  m2cpminvid2lem  22669  decpmatmulsumfsupp  22688  pmatcollpw1lem1  22689  pmatcollpw2lem  22692  pmatcollpwfi  22697  pm2mpf1  22714  mptcoe1matfsupp  22717  mp2pm2mplem4  22724  pm2mpmhmlem1  22733  pm2mp  22740  chpdmat  22756  chpscmat  22757  cpmidpmatlem3  22787  cayhamlem4  22803  neiptopnei  23047  cncnp  23195  isnrm2  23273  isreg2  23292  2ndcdisj  23371  islly2  23399  dislly  23412  kgen2ss  23470  ptbasfi  23496  ptclsg  23530  prdstopn  23543  txtube  23555  txlm  23563  isr0  23652  filuni  23800  alexsubALTlem3  23964  ptcmplem3  23969  ptcmplem4  23970  tsmsxplem1  24068  prdsmet  24285  metequiv2  24425  metcnpi3  24461  nmoleub  24646  rescncf  24817  cncfco  24827  evth  24885  lebnumlem3  24889  xlebnum  24891  nmoleub2lem2  25043  nmhmcn  25047  lmmcvg  25188  cmetcaulem  25215  caubl  25235  bcth3  25258  ovollb2lem  25416  ovoliunlem2  25431  ovolicc2lem3  25447  ovolicc2lem4  25448  nulmbl2  25464  volsup  25484  ioombl1lem4  25489  dyadmax  25526  vitalilem2  25537  vitalilem5  25540  mbfi1flimlem  25650  itg2seq  25670  itg2addlem  25686  itgcn  25773  limciun  25822  rolle  25921  dvfsumrlim  25965  itgsubst  25983  aannenlem1  26263  aalioulem3  26269  ulmcaulem  26330  ulmcau  26331  ulmss  26333  ulmbdd  26334  ulmcn  26335  ulmdvlem3  26338  mtest  26340  iblulm  26343  itgulm  26344  rlimcnp  26902  xrlimcnp  26905  rlimcxp  26911  o1cxp  26912  amgm  26928  lgambdd  26974  ftalem2  27011  isppw2  27052  mumullem2  27117  2sqlem6  27361  chtppilimlem2  27412  chtppilim  27413  pntrsumbnd2  27505  pntlem3  27547  nosupbnd1lem5  27651  noinfbnd1lem5  27666  noetasuplem4  27675  noetainflem4  27679  negsbdaylem  27998  mulsuniflem  28088  isperp2  28693  axeuclidlem  28940  axeuclid  28941  uhgrnbgr0nb  29332  vtxdginducedm1fi  29523  cusgrrusgr  29560  rusgrpropnb  29562  rusgrpropedg  29563  rusgrpropadjvtx  29564  upgrewlkle2  29585  wlkvtxiedg  29603  upgrwlkvtxedg  29623  uspgr2wlkeq  29624  redwlk  29649  wlkdlem2  29660  lfgrwlkprop  29664  2pthnloop  29709  upgr2pthnlp  29710  pthdlem1  29744  pthdlem2lem  29745  wlkiswwlks1  29845  wlkiswwlks2lem4  29850  wwlksm1edg  29859  wwlksnred  29870  clwwlkccatlem  29969  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  cusconngr  30171  eucrctshift  30223  2pthfrgr  30264  3cyclfrgr  30268  nmoub3i  30753  ubthlem1  30850  ubthlem3  30852  ocsh  31263  chintcli  31311  chscllem2  31618  nmopub2tALT  31889  nmfnleub2  31906  lnconi  32013  riesz1  32045  rnbra  32087  leopadd  32112  leopmuli  32113  leoptr  32117  dmdbr3  32285  dmdbr4  32286  dmdbr5  32288  mdsl0  32290  mdsymlem6  32388  cdj1i  32413  acunirnmpt  32641  xrge0infss  32743  isdrng4  33261  elrspunidl  33393  cmppcmp  33871  zarclsiin  33884  lmxrge0  33965  ftc2re  34611  cvmlift2lem12  35358  opnrebl2  36365  neibastop1  36403  neibastop2lem  36404  neibastop3  36406  finixpnum  37655  lindsenlbs  37665  matunitlindflem1  37666  matunitlindflem2  37667  ptrecube  37670  poimirlem26  37696  poimirlem27  37697  poimirlem29  37699  poimirlem30  37700  poimir  37703  heicant  37705  itg2addnclem  37721  itg2addnclem3  37723  itg2addnc  37724  filbcmb  37790  nninfnub  37801  geomcau  37809  sstotbnd2  37824  isbndx  37832  prdsbnd  37843  heibor1lem  37859  heiborlem1  37861  heibor  37871  rrncmslem  37882  intidl  38079  pclclN  40000  lauteq  40204  ltrnid  40244  mapdh9a  41898  primrootscoprmpow  42202  sticksstones3  42251  aks5lem5a  42294  aks5lem6  42295  fltaccoprm  42743  fltabcoprm  42745  flt4lem5  42753  elrfirn2  42799  isnacs3  42813  rencldnfilem  42923  kelac1  43166  naddgeoa  43497  neik0pk1imk0  44150  cvgdvgrat  44416  neglimc  45755  limsupub  45812  limsuppnflem  45818  limsupre3lem  45840  limsupvaluz2  45846  supcnvlimsup  45848  climuzlem  45851  liminfval2  45876  limsupgtlem  45885  liminflelimsupuz  45893  liminflimsupclim  45915  xlimpnfxnegmnf  45922  liminflimsupxrre  45925  xlimmnfv  45942  xlimpnfv  45946  stoweidlem7  46115  fourierdlem73  46287  sge0isum  46535  meaiuninc3v  46592  preimageiingt  46828  preimaleiinlt  46829  smflimlem3  46881  smflimlem4  46882  cfsetsnfsetfo  47170  2reu8i  47223  iccpartres  47528  uhgrimisgrgric  48041  grlictr  48125  clnbgr3stgrgrlim  48129  clnbgr3stgrgrlic  48130  upwlkwlk  48249  upgrwlkupwlk  48250  copisnmnd  48279  2zrngnmlid2  48367  ply1mulgsumlem1  48497  ply1mulgsumlem3  48499  ply1mulgsumlem4  48500  snlindsntor  48582  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849  iinfsubc  49169