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  3184  wereu2  5635  frpomin  6313  fveqressseq  7051  f1mpt  7236  isores3  7310  caofrss  7692  caoftrn  7694  sorpssuni  7708  sorpssint  7709  onint  7766  xpord3inddlem  8133  smogt  8336  fisupg  9235  ixpfi2  9301  fissuni  9308  indexfi  9311  fiinfg  9452  wemaplem2  9500  rankonidlem  9781  ac5num  9989  acni2  9999  acndom2  10007  alephle  10041  dfac5  10082  cfsmolem  10223  isf34lem7  10332  isf34lem6  10333  fin1a2s  10367  acncc  10393  ttukeylem6  10467  fpwwe2lem7  10590  gchina  10652  inar1  10728  tskord  10733  grudomon  10770  grur1a  10772  dedekind  11337  fimaxre  12127  fiminre  12130  uzwo  12870  xrsupsslem  13267  xrinfmsslem  13268  fsuppmapnn0fiub0  13958  rexanre  15313  rexuz3  15315  rexico  15320  cau3lem  15321  limsupval2  15446  rlim2lt  15463  rlim3  15464  lo1bdd2  15490  lo1bddrp  15491  o1lo1  15503  climrlim2  15513  2clim  15538  o1co  15552  rlimcn1  15554  rlimcn3  15556  climcn1  15558  climcn2  15559  subcn2  15561  o1of2  15579  rlimo1  15583  o1rlimmul  15585  lo1add  15593  lo1mul  15594  climsqz  15607  climsqz2  15608  rlimsqzlem  15615  lo1le  15618  climbdd  15638  caucvgrlem  15639  caucvgrlem2  15641  caurcvg2  15644  iseralt  15651  cvgcmp  15782  cvgcmpce  15784  gcdcllem1  16469  absproddvds  16587  coprmprod  16631  coprmproddvdslem  16632  pcfac  16870  pockthg  16877  infpnlem1  16881  prmreclem2  16888  prmreclem3  16889  vdwlem11  16962  vdwlem13  16964  vdwnnlem3  16968  isacs2  17614  acsfn1  17622  acsfn2  17624  catpropd  17670  drsdirfi  18266  ipodrsima  18500  isacs5  18507  mrelatglb  18519  mrelatlub  18521  isgrpinv  18925  dfgrp3e  18972  issubg4  19077  gsmsymgreqlem2  19361  finodsubmsubg  19497  gexdvds  19514  gexcl3  19517  sylow2blem3  19552  cyggeninv  19813  gsummptnn0fz  19916  dprdff  19944  issubdrg  20689  acsfn1p  20708  cygznlem3  21479  psdmul  22053  mptcoe1fsupp  22100  cply1coe0bi  22189  gsummoncoe1  22195  evls1fpws  22256  scmatdmat  22402  mdetdiagid  22487  mdetunilem9  22507  cpmatmcllem  22605  m2cpminvid2lem  22641  decpmatmulsumfsupp  22660  pmatcollpw1lem1  22661  pmatcollpw2lem  22664  pmatcollpwfi  22669  pm2mpf1  22686  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  pm2mpmhmlem1  22705  pm2mp  22712  chpdmat  22728  chpscmat  22729  cpmidpmatlem3  22759  cayhamlem4  22775  neiptopnei  23019  cncnp  23167  isnrm2  23245  isreg2  23264  2ndcdisj  23343  islly2  23371  dislly  23384  kgen2ss  23442  ptbasfi  23468  ptclsg  23502  prdstopn  23515  txtube  23527  txlm  23535  isr0  23624  filuni  23772  alexsubALTlem3  23936  ptcmplem3  23941  ptcmplem4  23942  tsmsxplem1  24040  prdsmet  24258  metequiv2  24398  metcnpi3  24434  nmoleub  24619  rescncf  24790  cncfco  24800  evth  24858  lebnumlem3  24862  xlebnum  24864  nmoleub2lem2  25016  nmhmcn  25020  lmmcvg  25161  cmetcaulem  25188  caubl  25208  bcth3  25231  ovollb2lem  25389  ovoliunlem2  25404  ovolicc2lem3  25420  ovolicc2lem4  25421  nulmbl2  25437  volsup  25457  ioombl1lem4  25462  dyadmax  25499  vitalilem2  25510  vitalilem5  25513  mbfi1flimlem  25623  itg2seq  25643  itg2addlem  25659  itgcn  25746  limciun  25795  rolle  25894  dvfsumrlim  25938  itgsubst  25956  aannenlem1  26236  aalioulem3  26242  ulmcaulem  26303  ulmcau  26304  ulmss  26306  ulmbdd  26307  ulmcn  26308  ulmdvlem3  26311  mtest  26313  iblulm  26316  itgulm  26317  rlimcnp  26875  xrlimcnp  26878  rlimcxp  26884  o1cxp  26885  amgm  26901  lgambdd  26947  ftalem2  26984  isppw2  27025  mumullem2  27090  2sqlem6  27334  chtppilimlem2  27385  chtppilim  27386  pntrsumbnd2  27478  pntlem3  27520  nosupbnd1lem5  27624  noinfbnd1lem5  27639  noetasuplem4  27648  noetainflem4  27652  negsbdaylem  27962  mulsuniflem  28052  isperp2  28642  axeuclidlem  28889  axeuclid  28890  uhgrnbgr0nb  29281  vtxdginducedm1fi  29472  cusgrrusgr  29509  rusgrpropnb  29511  rusgrpropedg  29512  rusgrpropadjvtx  29513  upgrewlkle2  29534  wlkvtxiedg  29553  upgrwlkvtxedg  29573  uspgr2wlkeq  29574  redwlk  29600  wlkdlem2  29611  lfgrwlkprop  29615  2pthnloop  29661  upgr2pthnlp  29662  pthdlem1  29696  pthdlem2lem  29697  wlkiswwlks1  29797  wlkiswwlks2lem4  29802  wwlksm1edg  29811  wwlksnred  29822  clwwlkccatlem  29918  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  cusconngr  30120  eucrctshift  30172  2pthfrgr  30213  3cyclfrgr  30217  nmoub3i  30702  ubthlem1  30799  ubthlem3  30801  ocsh  31212  chintcli  31260  chscllem2  31567  nmopub2tALT  31838  nmfnleub2  31855  lnconi  31962  riesz1  31994  rnbra  32036  leopadd  32061  leopmuli  32062  leoptr  32066  dmdbr3  32234  dmdbr4  32235  dmdbr5  32237  mdsl0  32239  mdsymlem6  32337  cdj1i  32362  acunirnmpt  32583  xrge0infss  32683  isdrng4  33245  elrspunidl  33399  cmppcmp  33848  zarclsiin  33861  lmxrge0  33942  ftc2re  34589  cvmlift2lem12  35301  opnrebl2  36309  neibastop1  36347  neibastop2lem  36348  neibastop3  36350  finixpnum  37599  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  ptrecube  37614  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem30  37644  poimir  37647  heicant  37649  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  filbcmb  37734  nninfnub  37745  geomcau  37753  sstotbnd2  37768  isbndx  37776  prdsbnd  37787  heibor1lem  37803  heiborlem1  37805  heibor  37815  rrncmslem  37826  intidl  38023  pclclN  39885  lauteq  40089  ltrnid  40129  mapdh9a  41783  primrootscoprmpow  42087  sticksstones3  42136  aks5lem5a  42179  aks5lem6  42180  fltaccoprm  42628  fltabcoprm  42630  flt4lem5  42638  elrfirn2  42684  isnacs3  42698  rencldnfilem  42808  kelac1  43052  naddgeoa  43383  neik0pk1imk0  44036  cvgdvgrat  44302  neglimc  45645  limsupub  45702  limsuppnflem  45708  limsupre3lem  45730  limsupvaluz2  45736  supcnvlimsup  45738  climuzlem  45741  liminfval2  45766  limsupgtlem  45775  liminflelimsupuz  45783  liminflimsupclim  45805  xlimpnfxnegmnf  45812  liminflimsupxrre  45815  xlimmnfv  45832  xlimpnfv  45836  stoweidlem7  46005  fourierdlem73  46177  sge0isum  46425  meaiuninc3v  46482  preimageiingt  46718  preimaleiinlt  46719  smflimlem3  46771  smflimlem4  46772  cfsetsnfsetfo  47061  2reu8i  47114  iccpartres  47419  uhgrimisgrgric  47931  grlictr  48007  clnbgr3stgrgrlic  48011  upwlkwlk  48127  upgrwlkupwlk  48128  copisnmnd  48157  2zrngnmlid2  48245  ply1mulgsumlem1  48375  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  snlindsntor  48460  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  iinfsubc  49047