Theorem ralimdva 3104

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

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

This theorem is referenced by:  ralimdv  3105  ralimdvva  3106  wereu2  5585  frpomin  6240  fveqressseq  6951  f1mpt  7128  isores3  7199  caofrss  7560  caoftrn  7562  sorpssuni  7576  sorpssint  7577  onint  7630  smogt  8182  fisupg  9023  ixpfi2  9078  fissuni  9085  indexfi  9088  fiinfg  9219  wemaplem2  9267  rankonidlem  9570  ac5num  9776  acni2  9786  acndom2  9794  alephle  9828  dfac5  9868  cfsmolem  10010  isf34lem7  10119  isf34lem6  10120  fin1a2s  10154  acncc  10180  ttukeylem6  10254  fpwwe2lem7  10377  gchina  10439  inar1  10515  tskord  10520  grudomon  10557  grur1a  10559  dedekind  11121  fimaxre  11902  fiminre  11905  uzwo  12633  xrsupsslem  13023  xrinfmsslem  13024  fsuppmapnn0fiub0  13694  rexanre  15039  rexuz3  15041  rexico  15046  cau3lem  15047  limsupval2  15170  rlim2lt  15187  rlim3  15188  lo1bdd2  15214  lo1bddrp  15215  o1lo1  15227  climrlim2  15237  2clim  15262  o1co  15276  rlimcn1  15278  rlimcn3  15280  climcn1  15282  climcn2  15283  subcn2  15285  o1of2  15303  rlimo1  15307  o1rlimmul  15309  lo1add  15317  lo1mul  15318  climsqz  15331  climsqz2  15332  rlimsqzlem  15341  lo1le  15344  climbdd  15364  caucvgrlem  15365  caucvgrlem2  15367  caurcvg2  15370  iseralt  15377  cvgcmp  15509  cvgcmpce  15511  gcdcllem1  16187  absproddvds  16303  coprmprod  16347  coprmproddvdslem  16348  pcfac  16581  pockthg  16588  infpnlem1  16592  prmreclem2  16599  prmreclem3  16600  vdwlem11  16673  vdwlem13  16675  vdwnnlem3  16679  isacs2  17343  acsfn1  17351  acsfn2  17353  catpropd  17399  drsdirfi  18004  ipodrsima  18240  isacs5  18247  mrelatglb  18259  mrelatlub  18261  isgrpinv  18613  dfgrp3e  18656  issubg4  18755  gsmsymgreqlem2  19020  gexdvds  19170  gexcl3  19173  sylow2blem3  19208  cyggeninv  19464  gsummptnn0fz  19568  dprdff  19596  issubdrg  20030  acsfn1p  20048  cygznlem3  20758  mptcoe1fsupp  21367  cply1coe0bi  21452  gsummoncoe1  21456  scmatdmat  21645  mdetdiagid  21730  mdetunilem9  21750  cpmatmcllem  21848  m2cpminvid2lem  21884  decpmatmulsumfsupp  21903  pmatcollpw1lem1  21904  pmatcollpw2lem  21907  pmatcollpwfi  21912  pm2mpf1  21929  mptcoe1matfsupp  21932  mp2pm2mplem4  21939  pm2mpmhmlem1  21948  pm2mp  21955  chpdmat  21971  chpscmat  21972  cpmidpmatlem3  22002  cayhamlem4  22018  neiptopnei  22264  cncnp  22412  isnrm2  22490  isreg2  22509  2ndcdisj  22588  islly2  22616  dislly  22629  kgen2ss  22687  ptbasfi  22713  ptclsg  22747  prdstopn  22760  txtube  22772  txlm  22780  isr0  22869  filuni  23017  alexsubALTlem3  23181  ptcmplem3  23186  ptcmplem4  23187  tsmsxplem1  23285  prdsmet  23504  metequiv2  23647  metcnpi3  23683  nmoleub  23876  rescncf  24041  cncfco  24051  evth  24103  lebnumlem3  24107  xlebnum  24109  nmoleub2lem2  24260  nmhmcn  24264  lmmcvg  24406  cmetcaulem  24433  caubl  24453  bcth3  24476  ovollb2lem  24633  ovoliunlem2  24648  ovolicc2lem3  24664  ovolicc2lem4  24665  nulmbl2  24681  volsup  24701  ioombl1lem4  24706  dyadmax  24743  vitalilem2  24754  vitalilem5  24757  mbfi1flimlem  24868  itg2seq  24888  itg2addlem  24904  itgcn  24990  limciun  25039  rolle  25135  dvfsumrlim  25176  itgsubst  25194  aannenlem1  25469  aalioulem3  25475  ulmcaulem  25534  ulmcau  25535  ulmss  25537  ulmbdd  25538  ulmcn  25539  ulmdvlem3  25542  mtest  25544  iblulm  25547  itgulm  25548  rlimcnp  26096  xrlimcnp  26099  rlimcxp  26104  o1cxp  26105  amgm  26121  lgambdd  26167  ftalem2  26204  isppw2  26245  mumullem2  26310  2sqlem6  26552  chtppilimlem2  26603  chtppilim  26604  pntrsumbnd2  26696  pntlem3  26738  isperp2  27057  axeuclidlem  27311  axeuclid  27312  uhgrnbgr0nb  27702  vtxdginducedm1fi  27892  cusgrrusgr  27929  rusgrpropnb  27931  rusgrpropedg  27932  rusgrpropadjvtx  27933  upgrewlkle2  27954  wlkvtxiedg  27972  upgrwlkvtxedg  27992  uspgr2wlkeq  27993  redwlk  28020  wlkdlem2  28031  lfgrwlkprop  28035  2pthnloop  28078  upgr2pthnlp  28079  pthdlem1  28113  pthdlem2lem  28114  wlkiswwlks1  28211  wlkiswwlks2lem4  28216  wwlksm1edg  28225  wwlksnred  28236  clwwlkccatlem  28332  clwlkclwwlklem2a  28341  clwlkclwwlklem2  28343  cusconngr  28534  eucrctshift  28586  2pthfrgr  28627  3cyclfrgr  28631  nmoub3i  29114  ubthlem1  29211  ubthlem3  29213  ocsh  29624  chintcli  29672  chscllem2  29979  nmopub2tALT  30250  nmfnleub2  30267  lnconi  30374  riesz1  30406  rnbra  30448  leopadd  30473  leopmuli  30474  leoptr  30478  dmdbr3  30646  dmdbr4  30647  dmdbr5  30649  mdsl0  30651  mdsymlem6  30749  cdj1i  30774  acunirnmpt  30975  xrge0infss  31062  elrspunidl  31585  cmppcmp  31787  zarclsiin  31800  lmxrge0  31881  ftc2re  32557  cvmlift2lem12  33255  nosupbnd1lem5  33894  noinfbnd1lem5  33909  noetasuplem4  33918  noetainflem4  33922  opnrebl2  34489  neibastop1  34527  neibastop2lem  34528  neibastop3  34530  finixpnum  35741  lindsenlbs  35751  matunitlindflem1  35752  matunitlindflem2  35753  ptrecube  35756  poimirlem26  35782  poimirlem27  35783  poimirlem29  35785  poimirlem30  35786  poimir  35789  heicant  35791  itg2addnclem  35807  itg2addnclem3  35809  itg2addnc  35810  filbcmb  35877  nninfnub  35888  geomcau  35896  sstotbnd2  35911  isbndx  35919  prdsbnd  35930  heibor1lem  35946  heiborlem1  35948  heibor  35958  rrncmslem  35969  intidl  36166  pclclN  37884  lauteq  38088  ltrnid  38128  mapdh9a  39782  sticksstones3  40084  fltaccoprm  40457  fltabcoprm  40459  flt4lem5  40467  elrfirn2  40498  isnacs3  40512  rencldnfilem  40622  kelac1  40868  neik0pk1imk0  41610  cvgdvgrat  41884  neglimc  43142  limsupub  43199  limsuppnflem  43205  limsupre3lem  43227  limsupvaluz2  43233  supcnvlimsup  43235  climuzlem  43238  liminfval2  43263  limsupgtlem  43272  liminflelimsupuz  43280  liminflimsupclim  43302  xlimpnfxnegmnf  43309  liminflimsupxrre  43312  xlimmnfv  43329  xlimpnfv  43333  stoweidlem7  43502  fourierdlem73  43674  sge0isum  43919  meaiuninc3v  43976  preimageiingt  44208  preimaleiinlt  44209  smflimlem3  44259  smflimlem4  44260  cfsetsnfsetfo  44505  2reu8i  44556  iccpartres  44822  upwlkwlk  45253  upgrwlkupwlk  45254  copisnmnd  45315  2zrngnmlid2  45461  ply1mulgsumlem1  45679  ply1mulgsumlem3  45681  ply1mulgsumlem4  45682  snlindsntor  45764  eenglngeehlnmlem1  46035  eenglngeehlnmlem2  46036