Theorem ralimdva 3145

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 3142	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

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

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

This theorem is referenced by:  ralimdv  3147  ralimdvva  3182  wereu2  5628  frpomin  6301  fveqressseq  7033  f1mpt  7218  isores3  7292  caofrss  7672  caoftrn  7674  sorpssuni  7688  sorpssint  7689  onint  7746  xpord3inddlem  8110  smogt  8313  fisupg  9211  ixpfi2  9277  fissuni  9284  indexfi  9287  fiinfg  9428  wemaplem2  9476  rankonidlem  9757  ac5num  9965  acni2  9975  acndom2  9983  alephle  10017  dfac5  10058  cfsmolem  10199  isf34lem7  10308  isf34lem6  10309  fin1a2s  10343  acncc  10369  ttukeylem6  10443  fpwwe2lem7  10566  gchina  10628  inar1  10704  tskord  10709  grudomon  10746  grur1a  10748  dedekind  11313  fimaxre  12103  fiminre  12106  uzwo  12846  xrsupsslem  13243  xrinfmsslem  13244  fsuppmapnn0fiub0  13934  rexanre  15289  rexuz3  15291  rexico  15296  cau3lem  15297  limsupval2  15422  rlim2lt  15439  rlim3  15440  lo1bdd2  15466  lo1bddrp  15467  o1lo1  15479  climrlim2  15489  2clim  15514  o1co  15528  rlimcn1  15530  rlimcn3  15532  climcn1  15534  climcn2  15535  subcn2  15537  o1of2  15555  rlimo1  15559  o1rlimmul  15561  lo1add  15569  lo1mul  15570  climsqz  15583  climsqz2  15584  rlimsqzlem  15591  lo1le  15594  climbdd  15614  caucvgrlem  15615  caucvgrlem2  15617  caurcvg2  15620  iseralt  15627  cvgcmp  15758  cvgcmpce  15760  gcdcllem1  16445  absproddvds  16563  coprmprod  16607  coprmproddvdslem  16608  pcfac  16846  pockthg  16853  infpnlem1  16857  prmreclem2  16864  prmreclem3  16865  vdwlem11  16938  vdwlem13  16940  vdwnnlem3  16944  isacs2  17594  acsfn1  17602  acsfn2  17604  catpropd  17650  drsdirfi  18246  ipodrsima  18482  isacs5  18489  mrelatglb  18501  mrelatlub  18503  isgrpinv  18907  dfgrp3e  18954  issubg4  19059  gsmsymgreqlem2  19345  finodsubmsubg  19481  gexdvds  19498  gexcl3  19501  sylow2blem3  19536  cyggeninv  19797  gsummptnn0fz  19900  dprdff  19928  issubdrg  20700  acsfn1p  20719  cygznlem3  21511  psdmul  22086  mptcoe1fsupp  22133  cply1coe0bi  22222  gsummoncoe1  22228  evls1fpws  22289  scmatdmat  22435  mdetdiagid  22520  mdetunilem9  22540  cpmatmcllem  22638  m2cpminvid2lem  22674  decpmatmulsumfsupp  22693  pmatcollpw1lem1  22694  pmatcollpw2lem  22697  pmatcollpwfi  22702  pm2mpf1  22719  mptcoe1matfsupp  22722  mp2pm2mplem4  22729  pm2mpmhmlem1  22738  pm2mp  22745  chpdmat  22761  chpscmat  22762  cpmidpmatlem3  22792  cayhamlem4  22808  neiptopnei  23052  cncnp  23200  isnrm2  23278  isreg2  23297  2ndcdisj  23376  islly2  23404  dislly  23417  kgen2ss  23475  ptbasfi  23501  ptclsg  23535  prdstopn  23548  txtube  23560  txlm  23568  isr0  23657  filuni  23805  alexsubALTlem3  23969  ptcmplem3  23974  ptcmplem4  23975  tsmsxplem1  24073  prdsmet  24291  metequiv2  24431  metcnpi3  24467  nmoleub  24652  rescncf  24823  cncfco  24833  evth  24891  lebnumlem3  24895  xlebnum  24897  nmoleub2lem2  25049  nmhmcn  25053  lmmcvg  25194  cmetcaulem  25221  caubl  25241  bcth3  25264  ovollb2lem  25422  ovoliunlem2  25437  ovolicc2lem3  25453  ovolicc2lem4  25454  nulmbl2  25470  volsup  25490  ioombl1lem4  25495  dyadmax  25532  vitalilem2  25543  vitalilem5  25546  mbfi1flimlem  25656  itg2seq  25676  itg2addlem  25692  itgcn  25779  limciun  25828  rolle  25927  dvfsumrlim  25971  itgsubst  25989  aannenlem1  26269  aalioulem3  26275  ulmcaulem  26336  ulmcau  26337  ulmss  26339  ulmbdd  26340  ulmcn  26341  ulmdvlem3  26344  mtest  26346  iblulm  26349  itgulm  26350  rlimcnp  26908  xrlimcnp  26911  rlimcxp  26917  o1cxp  26918  amgm  26934  lgambdd  26980  ftalem2  27017  isppw2  27058  mumullem2  27123  2sqlem6  27367  chtppilimlem2  27418  chtppilim  27419  pntrsumbnd2  27511  pntlem3  27553  nosupbnd1lem5  27657  noinfbnd1lem5  27672  noetasuplem4  27681  noetainflem4  27685  negsbdaylem  28002  mulsuniflem  28092  isperp2  28695  axeuclidlem  28942  axeuclid  28943  uhgrnbgr0nb  29334  vtxdginducedm1fi  29525  cusgrrusgr  29562  rusgrpropnb  29564  rusgrpropedg  29565  rusgrpropadjvtx  29566  upgrewlkle2  29587  wlkvtxiedg  29605  upgrwlkvtxedg  29625  uspgr2wlkeq  29626  redwlk  29651  wlkdlem2  29662  lfgrwlkprop  29666  2pthnloop  29711  upgr2pthnlp  29712  pthdlem1  29746  pthdlem2lem  29747  wlkiswwlks1  29847  wlkiswwlks2lem4  29852  wwlksm1edg  29861  wwlksnred  29872  clwwlkccatlem  29968  clwlkclwwlklem2a  29977  clwlkclwwlklem2  29979  cusconngr  30170  eucrctshift  30222  2pthfrgr  30263  3cyclfrgr  30267  nmoub3i  30752  ubthlem1  30849  ubthlem3  30851  ocsh  31262  chintcli  31310  chscllem2  31617  nmopub2tALT  31888  nmfnleub2  31905  lnconi  32012  riesz1  32044  rnbra  32086  leopadd  32111  leopmuli  32112  leoptr  32116  dmdbr3  32284  dmdbr4  32285  dmdbr5  32287  mdsl0  32289  mdsymlem6  32387  cdj1i  32412  acunirnmpt  32633  xrge0infss  32733  isdrng4  33261  elrspunidl  33392  cmppcmp  33841  zarclsiin  33854  lmxrge0  33935  ftc2re  34582  cvmlift2lem12  35294  opnrebl2  36302  neibastop1  36340  neibastop2lem  36341  neibastop3  36343  finixpnum  37592  lindsenlbs  37602  matunitlindflem1  37603  matunitlindflem2  37604  ptrecube  37607  poimirlem26  37633  poimirlem27  37634  poimirlem29  37636  poimirlem30  37637  poimir  37640  heicant  37642  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  filbcmb  37727  nninfnub  37738  geomcau  37746  sstotbnd2  37761  isbndx  37769  prdsbnd  37780  heibor1lem  37796  heiborlem1  37798  heibor  37808  rrncmslem  37819  intidl  38016  pclclN  39878  lauteq  40082  ltrnid  40122  mapdh9a  41776  primrootscoprmpow  42080  sticksstones3  42129  aks5lem5a  42172  aks5lem6  42173  fltaccoprm  42621  fltabcoprm  42623  flt4lem5  42631  elrfirn2  42677  isnacs3  42691  rencldnfilem  42801  kelac1  43045  naddgeoa  43376  neik0pk1imk0  44029  cvgdvgrat  44295  neglimc  45638  limsupub  45695  limsuppnflem  45701  limsupre3lem  45723  limsupvaluz2  45729  supcnvlimsup  45731  climuzlem  45734  liminfval2  45759  limsupgtlem  45768  liminflelimsupuz  45776  liminflimsupclim  45798  xlimpnfxnegmnf  45805  liminflimsupxrre  45808  xlimmnfv  45825  xlimpnfv  45829  stoweidlem7  45998  fourierdlem73  46170  sge0isum  46418  meaiuninc3v  46475  preimageiingt  46711  preimaleiinlt  46712  smflimlem3  46764  smflimlem4  46765  cfsetsnfsetfo  47054  2reu8i  47107  iccpartres  47412  uhgrimisgrgric  47924  grlictr  48000  clnbgr3stgrgrlic  48004  upwlkwlk  48120  upgrwlkupwlk  48121  copisnmnd  48150  2zrngnmlid2  48238  ply1mulgsumlem1  48368  ply1mulgsumlem3  48370  ply1mulgsumlem4  48371  snlindsntor  48453  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  iinfsubc  49040