Theorem ralimdva 3152

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 3149	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

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

This theorem is referenced by:  ralimdv  3154  ralimdvva  3191  wereu2  5651  frpomin  6329  fveqressseq  7068  f1mpt  7253  isores3  7327  caofrss  7708  caoftrn  7710  sorpssuni  7724  sorpssint  7725  onint  7782  xpord3inddlem  8151  smogt  8379  fisupg  9294  ixpfi2  9360  fissuni  9367  indexfi  9370  fiinfg  9511  wemaplem2  9559  rankonidlem  9840  ac5num  10048  acni2  10058  acndom2  10066  alephle  10100  dfac5  10141  cfsmolem  10282  isf34lem7  10391  isf34lem6  10392  fin1a2s  10426  acncc  10452  ttukeylem6  10526  fpwwe2lem7  10649  gchina  10711  inar1  10787  tskord  10792  grudomon  10829  grur1a  10831  dedekind  11396  fimaxre  12184  fiminre  12187  uzwo  12925  xrsupsslem  13321  xrinfmsslem  13322  fsuppmapnn0fiub0  14009  rexanre  15363  rexuz3  15365  rexico  15370  cau3lem  15371  limsupval2  15494  rlim2lt  15511  rlim3  15512  lo1bdd2  15538  lo1bddrp  15539  o1lo1  15551  climrlim2  15561  2clim  15586  o1co  15600  rlimcn1  15602  rlimcn3  15604  climcn1  15606  climcn2  15607  subcn2  15609  o1of2  15627  rlimo1  15631  o1rlimmul  15633  lo1add  15641  lo1mul  15642  climsqz  15655  climsqz2  15656  rlimsqzlem  15663  lo1le  15666  climbdd  15686  caucvgrlem  15687  caucvgrlem2  15689  caurcvg2  15692  iseralt  15699  cvgcmp  15830  cvgcmpce  15832  gcdcllem1  16516  absproddvds  16634  coprmprod  16678  coprmproddvdslem  16679  pcfac  16917  pockthg  16924  infpnlem1  16928  prmreclem2  16935  prmreclem3  16936  vdwlem11  17009  vdwlem13  17011  vdwnnlem3  17015  isacs2  17663  acsfn1  17671  acsfn2  17673  catpropd  17719  drsdirfi  18315  ipodrsima  18549  isacs5  18556  mrelatglb  18568  mrelatlub  18570  isgrpinv  18974  dfgrp3e  19021  issubg4  19126  gsmsymgreqlem2  19410  finodsubmsubg  19546  gexdvds  19563  gexcl3  19566  sylow2blem3  19601  cyggeninv  19862  gsummptnn0fz  19965  dprdff  19993  issubdrg  20738  acsfn1p  20757  cygznlem3  21528  psdmul  22102  mptcoe1fsupp  22149  cply1coe0bi  22238  gsummoncoe1  22244  evls1fpws  22305  scmatdmat  22451  mdetdiagid  22536  mdetunilem9  22556  cpmatmcllem  22654  m2cpminvid2lem  22690  decpmatmulsumfsupp  22709  pmatcollpw1lem1  22710  pmatcollpw2lem  22713  pmatcollpwfi  22718  pm2mpf1  22735  mptcoe1matfsupp  22738  mp2pm2mplem4  22745  pm2mpmhmlem1  22754  pm2mp  22761  chpdmat  22777  chpscmat  22778  cpmidpmatlem3  22808  cayhamlem4  22824  neiptopnei  23068  cncnp  23216  isnrm2  23294  isreg2  23313  2ndcdisj  23392  islly2  23420  dislly  23433  kgen2ss  23491  ptbasfi  23517  ptclsg  23551  prdstopn  23564  txtube  23576  txlm  23584  isr0  23673  filuni  23821  alexsubALTlem3  23985  ptcmplem3  23990  ptcmplem4  23991  tsmsxplem1  24089  prdsmet  24307  metequiv2  24447  metcnpi3  24483  nmoleub  24668  rescncf  24839  cncfco  24849  evth  24907  lebnumlem3  24911  xlebnum  24913  nmoleub2lem2  25065  nmhmcn  25069  lmmcvg  25211  cmetcaulem  25238  caubl  25258  bcth3  25281  ovollb2lem  25439  ovoliunlem2  25454  ovolicc2lem3  25470  ovolicc2lem4  25471  nulmbl2  25487  volsup  25507  ioombl1lem4  25512  dyadmax  25549  vitalilem2  25560  vitalilem5  25563  mbfi1flimlem  25673  itg2seq  25693  itg2addlem  25709  itgcn  25796  limciun  25845  rolle  25944  dvfsumrlim  25988  itgsubst  26006  aannenlem1  26286  aalioulem3  26292  ulmcaulem  26353  ulmcau  26354  ulmss  26356  ulmbdd  26357  ulmcn  26358  ulmdvlem3  26361  mtest  26363  iblulm  26366  itgulm  26367  rlimcnp  26925  xrlimcnp  26928  rlimcxp  26934  o1cxp  26935  amgm  26951  lgambdd  26997  ftalem2  27034  isppw2  27075  mumullem2  27140  2sqlem6  27384  chtppilimlem2  27435  chtppilim  27436  pntrsumbnd2  27528  pntlem3  27570  nosupbnd1lem5  27674  noinfbnd1lem5  27689  noetasuplem4  27698  noetainflem4  27702  negsbdaylem  28005  mulsuniflem  28092  isperp2  28640  axeuclidlem  28887  axeuclid  28888  uhgrnbgr0nb  29279  vtxdginducedm1fi  29470  cusgrrusgr  29507  rusgrpropnb  29509  rusgrpropedg  29510  rusgrpropadjvtx  29511  upgrewlkle2  29532  wlkvtxiedg  29551  upgrwlkvtxedg  29571  uspgr2wlkeq  29572  redwlk  29598  wlkdlem2  29609  lfgrwlkprop  29613  2pthnloop  29659  upgr2pthnlp  29660  pthdlem1  29694  pthdlem2lem  29695  wlkiswwlks1  29795  wlkiswwlks2lem4  29800  wwlksm1edg  29809  wwlksnred  29820  clwwlkccatlem  29916  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  cusconngr  30118  eucrctshift  30170  2pthfrgr  30211  3cyclfrgr  30215  nmoub3i  30700  ubthlem1  30797  ubthlem3  30799  ocsh  31210  chintcli  31258  chscllem2  31565  nmopub2tALT  31836  nmfnleub2  31853  lnconi  31960  riesz1  31992  rnbra  32034  leopadd  32059  leopmuli  32060  leoptr  32064  dmdbr3  32232  dmdbr4  32233  dmdbr5  32235  mdsl0  32237  mdsymlem6  32335  cdj1i  32360  acunirnmpt  32583  xrge0infss  32683  isdrng4  33235  elrspunidl  33389  cmppcmp  33835  zarclsiin  33848  lmxrge0  33929  ftc2re  34576  cvmlift2lem12  35282  opnrebl2  36285  neibastop1  36323  neibastop2lem  36324  neibastop3  36326  finixpnum  37575  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  ptrecube  37590  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem30  37620  poimir  37623  heicant  37625  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  filbcmb  37710  nninfnub  37721  geomcau  37729  sstotbnd2  37744  isbndx  37752  prdsbnd  37763  heibor1lem  37779  heiborlem1  37781  heibor  37791  rrncmslem  37802  intidl  37999  pclclN  39856  lauteq  40060  ltrnid  40100  mapdh9a  41754  primrootscoprmpow  42058  sticksstones3  42107  aks5lem5a  42150  aks5lem6  42151  fltaccoprm  42610  fltabcoprm  42612  flt4lem5  42620  elrfirn2  42666  isnacs3  42680  rencldnfilem  42790  kelac1  43034  naddgeoa  43365  neik0pk1imk0  44018  cvgdvgrat  44285  neglimc  45624  limsupub  45681  limsuppnflem  45687  limsupre3lem  45709  limsupvaluz2  45715  supcnvlimsup  45717  climuzlem  45720  liminfval2  45745  limsupgtlem  45754  liminflelimsupuz  45762  liminflimsupclim  45784  xlimpnfxnegmnf  45791  liminflimsupxrre  45794  xlimmnfv  45811  xlimpnfv  45815  stoweidlem7  45984  fourierdlem73  46156  sge0isum  46404  meaiuninc3v  46461  preimageiingt  46697  preimaleiinlt  46698  smflimlem3  46750  smflimlem4  46751  cfsetsnfsetfo  47037  2reu8i  47090  iccpartres  47380  uhgrimisgrgric  47892  grlictr  47968  clnbgr3stgrgrlic  47972  upwlkwlk  48062  upgrwlkupwlk  48063  copisnmnd  48092  2zrngnmlid2  48180  ply1mulgsumlem1  48310  ply1mulgsumlem3  48312  ply1mulgsumlem4  48313  snlindsntor  48395  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  iinfsubc  48973