Theorem ralimdva 3166

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3060

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3061

This theorem is referenced by:  ralimdv  3168  ralimdvva  3203  wereu2  5673  frpomin  6341  fveqressseq  7081  f1mpt  7263  isores3  7335  caofrss  7710  caoftrn  7712  sorpssuni  7726  sorpssint  7727  onint  7782  xpord3inddlem  8145  smogt  8373  fisupg  9297  ixpfi2  9356  fissuni  9363  indexfi  9366  fiinfg  9500  wemaplem2  9548  rankonidlem  9829  ac5num  10037  acni2  10047  acndom2  10055  alephle  10089  dfac5  10129  cfsmolem  10271  isf34lem7  10380  isf34lem6  10381  fin1a2s  10415  acncc  10441  ttukeylem6  10515  fpwwe2lem7  10638  gchina  10700  inar1  10776  tskord  10781  grudomon  10818  grur1a  10820  dedekind  11384  fimaxre  12165  fiminre  12168  uzwo  12902  xrsupsslem  13293  xrinfmsslem  13294  fsuppmapnn0fiub0  13965  rexanre  15300  rexuz3  15302  rexico  15307  cau3lem  15308  limsupval2  15431  rlim2lt  15448  rlim3  15449  lo1bdd2  15475  lo1bddrp  15476  o1lo1  15488  climrlim2  15498  2clim  15523  o1co  15537  rlimcn1  15539  rlimcn3  15541  climcn1  15543  climcn2  15544  subcn2  15546  o1of2  15564  rlimo1  15568  o1rlimmul  15570  lo1add  15578  lo1mul  15579  climsqz  15592  climsqz2  15593  rlimsqzlem  15602  lo1le  15605  climbdd  15625  caucvgrlem  15626  caucvgrlem2  15628  caurcvg2  15631  iseralt  15638  cvgcmp  15769  cvgcmpce  15771  gcdcllem1  16447  absproddvds  16561  coprmprod  16605  coprmproddvdslem  16606  pcfac  16839  pockthg  16846  infpnlem1  16850  prmreclem2  16857  prmreclem3  16858  vdwlem11  16931  vdwlem13  16933  vdwnnlem3  16937  isacs2  17604  acsfn1  17612  acsfn2  17614  catpropd  17660  drsdirfi  18268  ipodrsima  18504  isacs5  18511  mrelatglb  18523  mrelatlub  18525  isgrpinv  18921  dfgrp3e  18966  issubg4  19068  gsmsymgreqlem2  19347  finodsubmsubg  19483  gexdvds  19500  gexcl3  19503  sylow2blem3  19538  cyggeninv  19799  gsummptnn0fz  19902  dprdff  19930  issubdrg  20627  acsfn1p  20646  cygznlem3  21435  mptcoe1fsupp  22058  cply1coe0bi  22144  gsummoncoe1  22148  scmatdmat  22337  mdetdiagid  22422  mdetunilem9  22442  cpmatmcllem  22540  m2cpminvid2lem  22576  decpmatmulsumfsupp  22595  pmatcollpw1lem1  22596  pmatcollpw2lem  22599  pmatcollpwfi  22604  pm2mpf1  22621  mptcoe1matfsupp  22624  mp2pm2mplem4  22631  pm2mpmhmlem1  22640  pm2mp  22647  chpdmat  22663  chpscmat  22664  cpmidpmatlem3  22694  cayhamlem4  22710  neiptopnei  22956  cncnp  23104  isnrm2  23182  isreg2  23201  2ndcdisj  23280  islly2  23308  dislly  23321  kgen2ss  23379  ptbasfi  23405  ptclsg  23439  prdstopn  23452  txtube  23464  txlm  23472  isr0  23561  filuni  23709  alexsubALTlem3  23873  ptcmplem3  23878  ptcmplem4  23879  tsmsxplem1  23977  prdsmet  24196  metequiv2  24339  metcnpi3  24375  nmoleub  24568  rescncf  24737  cncfco  24747  evth  24805  lebnumlem3  24809  xlebnum  24811  nmoleub2lem2  24963  nmhmcn  24967  lmmcvg  25109  cmetcaulem  25136  caubl  25156  bcth3  25179  ovollb2lem  25337  ovoliunlem2  25352  ovolicc2lem3  25368  ovolicc2lem4  25369  nulmbl2  25385  volsup  25405  ioombl1lem4  25410  dyadmax  25447  vitalilem2  25458  vitalilem5  25461  mbfi1flimlem  25572  itg2seq  25592  itg2addlem  25608  itgcn  25694  limciun  25743  rolle  25842  dvfsumrlim  25886  itgsubst  25904  aannenlem1  26180  aalioulem3  26186  ulmcaulem  26245  ulmcau  26246  ulmss  26248  ulmbdd  26249  ulmcn  26250  ulmdvlem3  26253  mtest  26255  iblulm  26258  itgulm  26259  rlimcnp  26811  xrlimcnp  26814  rlimcxp  26819  o1cxp  26820  amgm  26836  lgambdd  26882  ftalem2  26919  isppw2  26960  mumullem2  27025  2sqlem6  27269  chtppilimlem2  27320  chtppilim  27321  pntrsumbnd2  27413  pntlem3  27455  nosupbnd1lem5  27558  noinfbnd1lem5  27573  noetasuplem4  27582  noetainflem4  27586  negsbdaylem  27881  mulsuniflem  27962  isperp2  28399  axeuclidlem  28653  axeuclid  28654  uhgrnbgr0nb  29044  vtxdginducedm1fi  29234  cusgrrusgr  29271  rusgrpropnb  29273  rusgrpropedg  29274  rusgrpropadjvtx  29275  upgrewlkle2  29296  wlkvtxiedg  29315  upgrwlkvtxedg  29335  uspgr2wlkeq  29336  redwlk  29362  wlkdlem2  29373  lfgrwlkprop  29377  2pthnloop  29421  upgr2pthnlp  29422  pthdlem1  29456  pthdlem2lem  29457  wlkiswwlks1  29554  wlkiswwlks2lem4  29559  wwlksm1edg  29568  wwlksnred  29579  clwwlkccatlem  29675  clwlkclwwlklem2a  29684  clwlkclwwlklem2  29686  cusconngr  29877  eucrctshift  29929  2pthfrgr  29970  3cyclfrgr  29974  nmoub3i  30459  ubthlem1  30556  ubthlem3  30558  ocsh  30969  chintcli  31017  chscllem2  31324  nmopub2tALT  31595  nmfnleub2  31612  lnconi  31719  riesz1  31751  rnbra  31793  leopadd  31818  leopmuli  31819  leoptr  31823  dmdbr3  31991  dmdbr4  31992  dmdbr5  31994  mdsl0  31996  mdsymlem6  32094  cdj1i  32119  acunirnmpt  32317  xrge0infss  32406  isdrng4  32831  elrspunidl  32986  evls1fpws  33086  cmppcmp  33302  zarclsiin  33315  lmxrge0  33396  ftc2re  34074  cvmlift2lem12  34769  opnrebl2  35670  neibastop1  35708  neibastop2lem  35709  neibastop3  35711  finixpnum  36937  lindsenlbs  36947  matunitlindflem1  36948  matunitlindflem2  36949  ptrecube  36952  poimirlem26  36978  poimirlem27  36979  poimirlem29  36981  poimirlem30  36982  poimir  36985  heicant  36987  itg2addnclem  37003  itg2addnclem3  37005  itg2addnc  37006  filbcmb  37072  nninfnub  37083  geomcau  37091  sstotbnd2  37106  isbndx  37114  prdsbnd  37125  heibor1lem  37141  heiborlem1  37143  heibor  37153  rrncmslem  37164  intidl  37361  pclclN  39226  lauteq  39430  ltrnid  39470  mapdh9a  41124  sticksstones3  41431  fltaccoprm  41845  fltabcoprm  41847  flt4lem5  41855  elrfirn2  41897  isnacs3  41911  rencldnfilem  42021  kelac1  42268  naddgeoa  42608  neik0pk1imk0  43261  cvgdvgrat  43535  neglimc  44822  limsupub  44879  limsuppnflem  44885  limsupre3lem  44907  limsupvaluz2  44913  supcnvlimsup  44915  climuzlem  44918  liminfval2  44943  limsupgtlem  44952  liminflelimsupuz  44960  liminflimsupclim  44982  xlimpnfxnegmnf  44989  liminflimsupxrre  44992  xlimmnfv  45009  xlimpnfv  45013  stoweidlem7  45182  fourierdlem73  45354  sge0isum  45602  meaiuninc3v  45659  preimageiingt  45895  preimaleiinlt  45896  smflimlem3  45948  smflimlem4  45949  cfsetsnfsetfo  46229  2reu8i  46280  iccpartres  46545  upwlkwlk  46976  upgrwlkupwlk  46977  copisnmnd  47006  2zrngnmlid2  47094  ply1mulgsumlem1  47229  ply1mulgsumlem3  47231  ply1mulgsumlem4  47232  snlindsntor  47314  eenglngeehlnmlem1  47585  eenglngeehlnmlem2  47586