Theorem ralimdva 3150

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  ralimdv  3152  ralimdvva  3185  wereu2  5622  frpomin  6299  fveqressseq  7026  f1mpt  7210  isores3  7284  caofrss  7664  caoftrn  7666  sorpssuni  7680  sorpssint  7681  onint  7738  xpord3inddlem  8098  smogt  8301  fisupg  9192  ixpfi2  9254  fissuni  9261  indexfi  9264  fiinfg  9408  wemaplem2  9456  rankonidlem  9746  ac5num  9952  acni2  9962  acndom2  9970  alephle  10004  dfac5  10045  cfsmolem  10186  isf34lem7  10295  isf34lem6  10296  fin1a2s  10330  acncc  10356  ttukeylem6  10430  fpwwe2lem7  10554  gchina  10616  inar1  10692  tskord  10697  grudomon  10734  grur1a  10736  dedekind  11303  fimaxre  12094  fiminre  12097  uzwo  12855  xrsupsslem  13253  xrinfmsslem  13254  fsuppmapnn0fiub0  13949  rexanre  15303  rexuz3  15305  rexico  15310  cau3lem  15311  limsupval2  15436  rlim2lt  15453  rlim3  15454  lo1bdd2  15480  lo1bddrp  15481  o1lo1  15493  climrlim2  15503  2clim  15528  o1co  15542  rlimcn1  15544  rlimcn3  15546  climcn1  15548  climcn2  15549  subcn2  15551  o1of2  15569  rlimo1  15573  o1rlimmul  15575  lo1add  15583  lo1mul  15584  climsqz  15597  climsqz2  15598  rlimsqzlem  15605  lo1le  15608  climbdd  15628  caucvgrlem  15629  caucvgrlem2  15631  caurcvg2  15634  iseralt  15641  cvgcmp  15773  cvgcmpce  15775  gcdcllem1  16462  absproddvds  16580  coprmprod  16624  coprmproddvdslem  16625  pcfac  16864  pockthg  16871  infpnlem1  16875  prmreclem2  16882  prmreclem3  16883  vdwlem11  16956  vdwlem13  16958  vdwnnlem3  16962  isacs2  17613  acsfn1  17621  acsfn2  17623  catpropd  17669  drsdirfi  18265  ipodrsima  18501  isacs5  18508  mrelatglb  18520  mrelatlub  18522  isgrpinv  18963  dfgrp3e  19010  issubg4  19115  gsmsymgreqlem2  19400  finodsubmsubg  19536  gexdvds  19553  gexcl3  19556  sylow2blem3  19591  cyggeninv  19852  gsummptnn0fz  19955  dprdff  19983  issubdrg  20751  acsfn1p  20770  cygznlem3  21562  psdmul  22145  mptcoe1fsupp  22192  cply1coe0bi  22280  gsummoncoe1  22286  evls1fpws  22347  scmatdmat  22493  mdetdiagid  22578  mdetunilem9  22598  cpmatmcllem  22696  m2cpminvid2lem  22732  decpmatmulsumfsupp  22751  pmatcollpw1lem1  22752  pmatcollpw2lem  22755  pmatcollpwfi  22760  pm2mpf1  22777  mptcoe1matfsupp  22780  mp2pm2mplem4  22787  pm2mpmhmlem1  22796  pm2mp  22803  chpdmat  22819  chpscmat  22820  cpmidpmatlem3  22850  cayhamlem4  22866  neiptopnei  23110  cncnp  23258  isnrm2  23336  isreg2  23355  2ndcdisj  23434  islly2  23462  dislly  23475  kgen2ss  23533  ptbasfi  23559  ptclsg  23593  prdstopn  23606  txtube  23618  txlm  23626  isr0  23715  filuni  23863  alexsubALTlem3  24027  ptcmplem3  24032  ptcmplem4  24033  tsmsxplem1  24131  prdsmet  24348  metequiv2  24488  metcnpi3  24524  nmoleub  24709  rescncf  24877  cncfco  24887  evth  24939  lebnumlem3  24943  xlebnum  24945  nmoleub2lem2  25096  nmhmcn  25100  lmmcvg  25241  cmetcaulem  25268  caubl  25288  bcth3  25311  ovollb2lem  25468  ovoliunlem2  25483  ovolicc2lem3  25499  ovolicc2lem4  25500  nulmbl2  25516  volsup  25536  ioombl1lem4  25541  dyadmax  25578  vitalilem2  25589  vitalilem5  25592  mbfi1flimlem  25702  itg2seq  25722  itg2addlem  25738  itgcn  25825  limciun  25874  rolle  25970  dvfsumrlim  26011  itgsubst  26029  aannenlem1  26308  aalioulem3  26314  ulmcaulem  26375  ulmcau  26376  ulmss  26378  ulmbdd  26379  ulmcn  26380  ulmdvlem3  26383  mtest  26385  iblulm  26388  itgulm  26389  rlimcnp  26945  xrlimcnp  26948  rlimcxp  26954  o1cxp  26955  amgm  26971  lgambdd  27017  ftalem2  27054  isppw2  27095  mumullem2  27160  2sqlem6  27403  chtppilimlem2  27454  chtppilim  27455  pntrsumbnd2  27547  pntlem3  27589  nosupbnd1lem5  27693  noinfbnd1lem5  27708  noetasuplem4  27717  noetainflem4  27721  negbdaylem  28065  mulsuniflem  28158  elreno2  28504  isperp2  28800  axeuclidlem  29048  axeuclid  29049  uhgrnbgr0nb  29440  vtxdginducedm1fi  29631  cusgrrusgr  29668  rusgrpropnb  29670  rusgrpropedg  29671  rusgrpropadjvtx  29672  upgrewlkle2  29693  wlkvtxiedg  29711  upgrwlkvtxedg  29731  uspgr2wlkeq  29732  redwlk  29757  wlkdlem2  29768  lfgrwlkprop  29772  2pthnloop  29817  upgr2pthnlp  29818  pthdlem1  29852  pthdlem2lem  29853  wlkiswwlks1  29953  wlkiswwlks2lem4  29958  wwlksm1edg  29967  wwlksnred  29978  clwwlkccatlem  30077  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  cusconngr  30279  eucrctshift  30331  2pthfrgr  30372  3cyclfrgr  30376  nmoub3i  30862  ubthlem1  30959  ubthlem3  30961  ocsh  31372  chintcli  31420  chscllem2  31727  nmopub2tALT  31998  nmfnleub2  32015  lnconi  32122  riesz1  32154  rnbra  32196  leopadd  32221  leopmuli  32222  leoptr  32226  dmdbr3  32394  dmdbr4  32395  dmdbr5  32397  mdsl0  32399  mdsymlem6  32497  cdj1i  32522  acunirnmpt  32750  xrge0infss  32851  isdrng4  33374  elrspunidl  33506  cmppcmp  34021  zarclsiin  34034  lmxrge0  34115  ftc2re  34761  cvmlift2lem12  35515  opnrebl2  36522  neibastop1  36560  neibastop2lem  36561  neibastop3  36563  finixpnum  37943  lindsenlbs  37953  matunitlindflem1  37954  matunitlindflem2  37955  ptrecube  37958  poimirlem26  37984  poimirlem27  37985  poimirlem29  37987  poimirlem30  37988  poimir  37991  heicant  37993  itg2addnclem  38009  itg2addnclem3  38011  itg2addnc  38012  filbcmb  38078  nninfnub  38089  geomcau  38097  sstotbnd2  38112  isbndx  38120  prdsbnd  38131  heibor1lem  38147  heiborlem1  38149  heibor  38159  rrncmslem  38170  intidl  38367  pclclN  40354  lauteq  40558  ltrnid  40598  mapdh9a  42252  primrootscoprmpow  42555  sticksstones3  42604  aks5lem5a  42647  aks5lem6  42648  fltaccoprm  43090  fltabcoprm  43092  flt4lem5  43100  elrfirn2  43145  isnacs3  43159  rencldnfilem  43269  kelac1  43512  naddgeoa  43843  neik0pk1imk0  44495  cvgdvgrat  44761  neglimc  46096  limsupub  46153  limsuppnflem  46159  limsupre3lem  46181  limsupvaluz2  46187  supcnvlimsup  46189  climuzlem  46192  liminfval2  46217  limsupgtlem  46226  liminflelimsupuz  46234  liminflimsupclim  46256  xlimpnfxnegmnf  46263  liminflimsupxrre  46266  xlimmnfv  46283  xlimpnfv  46287  stoweidlem7  46456  fourierdlem73  46628  sge0isum  46876  meaiuninc3v  46933  preimageiingt  47169  preimaleiinlt  47170  smflimlem3  47222  smflimlem4  47223  cfsetsnfsetfo  47523  2reu8i  47576  iccpartres  47893  uhgrimisgrgric  48422  grlictr  48506  clnbgr3stgrgrlim  48510  clnbgr3stgrgrlic  48511  upwlkwlk  48630  upgrwlkupwlk  48631  copisnmnd  48660  2zrngnmlid2  48748  ply1mulgsumlem1  48877  ply1mulgsumlem3  48879  ply1mulgsumlem4  48880  snlindsntor  48962  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  iinfsubc  49548