Theorem ralimdva 3178

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  ralimdv  3180  ralimdvva  3213  wereu2  5655  frpomin  6369  fveqressseq  7111  f1mpt  7296  isores3  7374  caofrss  7764  caoftrn  7766  sorpssuni  7780  sorpssint  7781  onint  7838  xpord3inddlem  8208  smogt  8413  fisupg  9317  ixpfi2  9377  fissuni  9384  indexfi  9387  fiinfg  9530  wemaplem2  9578  rankonidlem  9875  ac5num  10154  acni2  10164  acndom2  10172  alephle  10206  dfac5  10246  cfsmolem  10387  isf34lem7  10496  isf34lem6  10497  fin1a2s  10531  acncc  10557  ttukeylem6  10631  fpwwe2lem7  10761  gchina  10823  inar1  10899  tskord  10904  grudomon  10941  grur1a  10943  dedekind  11512  fimaxre  12301  fiminre  12304  uzwo  13078  xrsupsslem  13477  xrinfmsslem  13478  fsuppmapnn0fiub0  14176  rexanre  15558  rexuz3  15560  rexico  15565  cau3lem  15566  limsupval2  15691  rlim2lt  15708  rlim3  15709  lo1bdd2  15735  lo1bddrp  15736  o1lo1  15748  climrlim2  15758  2clim  15783  o1co  15797  rlimcn1  15799  rlimcn3  15801  climcn1  15803  climcn2  15804  subcn2  15806  o1of2  15824  rlimo1  15828  o1rlimmul  15830  lo1add  15838  lo1mul  15839  climsqz  15852  climsqz2  15853  rlimsqzlem  15860  lo1le  15863  climbdd  15883  caucvgrlem  15884  caucvgrlem2  15886  caurcvg2  15889  iseralt  15896  cvgcmp  16027  cvgcmpce  16029  gcdcllem1  16713  absproddvds  16836  coprmprod  16880  coprmproddvdslem  16881  pcfac  17121  pockthg  17128  infpnlem1  17132  prmreclem2  17139  prmreclem3  17140  vdwlem11  17213  vdwlem13  17215  vdwnnlem3  17219  isacs2  17877  acsfn1  17885  acsfn2  17887  catpropd  17933  drsdirfi  18529  ipodrsima  18765  isacs5  18772  mrelatglb  18784  mrelatlub  18786  isgrpinv  19254  dfgrp3e  19300  issubg4  19406  gsmsymgreqlem2  19696  finodsubmsubg  19832  gexdvds  19849  gexcl3  19852  sylow2blem3  19887  cyggeninv  20148  gsummptnn0fz  20251  dprdff  20279  isdrng4  21043  issubdrg  21088  acsfn1p  21107  cygznlem3  21930  lindsenlbs  22212  psdmul  22542  mptcoe1fsupp  22588  cply1coe0bi  22675  gsummoncoe1  22681  evls1fpws  22742  scmatdmat  22885  mdetdiagid  22970  mdetunilem9  22990  matunitlindflem1  23049  matunitlindflem2  23050  cpmatmcllem  23091  m2cpminvid2lem  23127  decpmatmulsumfsupp  23146  pmatcollpw1lem1  23147  pmatcollpw2lem  23150  pmatcollpwfi  23155  pm2mpf1  23172  mptcoe1matfsupp  23175  mp2pm2mplem4  23182  pm2mpmhmlem1  23191  pm2mp  23198  chpdmat  23214  chpscmat  23215  cpmidpmatlem3  23245  cayhamlem4  23261  neiptopnei  23505  cncnp  23653  isnrm2  23731  isreg2  23750  2ndcdisj  23830  islly2  23858  dislly  23871  kgen2ss  23929  ptbasfi  23955  ptclsg  23989  prdstopn  24002  txtube  24014  txlm  24022  isr0  24111  filuni  24259  alexsubALTlem3  24423  ptcmplem3  24428  ptcmplem4  24429  tsmsxplem1  24527  prdsmet  24744  metequiv2  24884  metcnpi3  24920  nmoleub  25105  rescncf  25273  cncfco  25283  evth  25335  lebnumlem3  25339  xlebnum  25341  nmoleub2lem2  25492  nmhmcn  25496  lmmcvg  25637  cmetcaulem  25664  caubl  25684  bcth3  25707  ovollb2lem  25864  ovoliunlem2  25879  ovolicc2lem3  25895  ovolicc2lem4  25896  nulmbl2  25912  volsup  25932  ioombl1lem4  25937  dyadmax  25974  vitalilem2  25985  vitalilem5  25988  mbfi1flimlem  26098  itg2seq  26118  itg2addlem  26134  itgcn  26220  limciun  26269  rolle  26365  dvfsumrlim  26406  itgsubst  26424  aannenlem1  26712  aalioulem3  26718  ulmcaulem  26778  ulmcau  26779  ulmss  26781  ulmbdd  26782  ulmcn  26783  ulmdvlem3  26786  mtest  26788  iblulm  26791  itgulm  26792  rlimcnp  27350  xrlimcnp  27353  rlimcxp  27358  o1cxp  27359  amgm  27375  lgambdd  27421  ftalem2  27458  isppw2  27499  mumullem2  27564  2sqlem6  27807  chtppilimlem2  27858  chtppilim  27859  pntrsumbnd2  27951  pntlem3  27993  fltaccoprm  28029  fltabcoprm  28031  flt4lem5  28037  nosupbnd1lem5  28126  noinfbnd1lem5  28141  noetasuplem4  28150  noetainflem4  28154  negbdaylem  28499  mulsuniflem  28592  elreno2  28938  isperp2  29247  axeuclidlem  29597  axeuclid  29598  uhgrnbgr0nb  29992  vtxdginducedm1fi  30182  cusgrrusgr  30219  rusgrpropnb  30221  rusgrpropedg  30222  rusgrpropadjvtx  30223  upgrewlkle2  30244  wlkvtxiedg  30262  upgrwlkvtxedg  30282  uspgr2wlkeq  30283  redwlk  30308  wlkdlem2  30319  lfgrwlkprop  30327  2pthnloop  30374  upgr2pthnlp  30375  pthdlem1  30409  pthdlem2lem  30410  wlkiswwlks1  30513  wlkiswwlks2lem4  30518  wwlksm1edg  30527  wwlksnred  30538  clwwlkccatlem  30637  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  cusconngr  30849  eucrctshift  30901  2pthfrgr  30942  3cyclfrgr  30946  nmoub3i  31432  ubthlem1  31529  ubthlem3  31531  ocsh  31942  chintcli  31990  chscllem2  32297  nmopub2tALT  32568  nmfnleub2  32585  lnconi  32692  riesz1  32724  rnbra  32766  leopadd  32791  leopmuli  32792  leoptr  32796  dmdbr3  32964  dmdbr4  32965  dmdbr5  32967  mdsl0  32969  mdsymlem6  33067  cdj1i  33092  acunirnmpt  33351  xrge0infss  33448  elrspunidl  34082  dflring2  34129  cmppcmp  34601  zarclsiin  34614  lmxrge0  34695  ftc2re  35338  cvmlift2lem12  36287  nmulrid  37161  opnrebl2  37324  neibastop1  37362  neibastop2lem  37363  neibastop3  37365  finixpnum  38796  ptrecube  38806  poimirlem26  38832  poimirlem27  38833  poimirlem29  38835  poimirlem30  38836  poimir  38839  heicant  38841  itg2addnclem  38857  itg2addnclem3  38859  itg2addnc  38860  filbcmb  38940  nninfnub  38951  geomcau  38959  sstotbnd2  38974  isbndx  38982  prdsbnd  38993  heibor1lem  39009  heiborlem1  39011  heibor  39021  rrncmslem  39032  intidl  39229  pclclN  41214  lauteq  41418  ltrnid  41458  mapdh9a  43112  primrootscoprmpow  43415  sticksstones3  43464  aks5lem5a  43507  aks5lem6  43508  elrfirn2  43973  isnacs3  43987  rencldnfilem  44093  kelac1  44331  naddgeoa  44657  neik0pk1imk0  45308  cvgdvgrat  45558  neglimc  46930  limsupub  46987  limsuppnflem  46993  limsupre3lem  47015  limsupvaluz2  47021  supcnvlimsup  47023  climuzlem  47026  liminfval2  47051  limsupgtlem  47060  liminflelimsupuz  47068  liminflimsupclim  47090  xlimpnfxnegmnf  47097  liminflimsupxrre  47100  xlimmnfv  47117  xlimpnfv  47121  stoweidlem7  47290  fourierdlem73  47462  sge0isum  47710  meaiuninc3v  47767  preimageiingt  48003  preimaleiinlt  48004  smflimlem3  48056  smflimlem4  48057  cfsetsnfsetfo  48403  2reu8i  48457  iccpartres  48773  uhgrimisgrgric  49302  grlictr  49386  clnbgr3stgrgrlim  49390  clnbgr3stgrgrlic  49391  upwlkwlk  49510  upgrwlkupwlk  49511  copisnmnd  49539  2zrngnmlid2  49627  ply1mulgsumlem1  49829  ply1mulgsumlem3  49831  ply1mulgsumlem4  49832  snlindsntor  49914  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  iinfsubc  50503