Theorem ralimdva 3141

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 3138	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  3143  ralimdvva  3176  wereu2  5616  frpomin  6288  fveqressseq  7013  f1mpt  7198  isores3  7272  caofrss  7652  caoftrn  7654  sorpssuni  7668  sorpssint  7669  onint  7726  xpord3inddlem  8087  smogt  8290  fisupg  9177  ixpfi2  9240  fissuni  9247  indexfi  9250  fiinfg  9391  wemaplem2  9439  rankonidlem  9724  ac5num  9930  acni2  9940  acndom2  9948  alephle  9982  dfac5  10023  cfsmolem  10164  isf34lem7  10273  isf34lem6  10274  fin1a2s  10308  acncc  10334  ttukeylem6  10408  fpwwe2lem7  10531  gchina  10593  inar1  10669  tskord  10674  grudomon  10711  grur1a  10713  dedekind  11279  fimaxre  12069  fiminre  12072  uzwo  12812  xrsupsslem  13209  xrinfmsslem  13210  fsuppmapnn0fiub0  13900  rexanre  15254  rexuz3  15256  rexico  15261  cau3lem  15262  limsupval2  15387  rlim2lt  15404  rlim3  15405  lo1bdd2  15431  lo1bddrp  15432  o1lo1  15444  climrlim2  15454  2clim  15479  o1co  15493  rlimcn1  15495  rlimcn3  15497  climcn1  15499  climcn2  15500  subcn2  15502  o1of2  15520  rlimo1  15524  o1rlimmul  15526  lo1add  15534  lo1mul  15535  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  lo1le  15559  climbdd  15579  caucvgrlem  15580  caucvgrlem2  15582  caurcvg2  15585  iseralt  15592  cvgcmp  15723  cvgcmpce  15725  gcdcllem1  16410  absproddvds  16528  coprmprod  16572  coprmproddvdslem  16573  pcfac  16811  pockthg  16818  infpnlem1  16822  prmreclem2  16829  prmreclem3  16830  vdwlem11  16903  vdwlem13  16905  vdwnnlem3  16909  isacs2  17559  acsfn1  17567  acsfn2  17569  catpropd  17615  drsdirfi  18211  ipodrsima  18447  isacs5  18454  mrelatglb  18466  mrelatlub  18468  isgrpinv  18872  dfgrp3e  18919  issubg4  19024  gsmsymgreqlem2  19310  finodsubmsubg  19446  gexdvds  19463  gexcl3  19466  sylow2blem3  19501  cyggeninv  19762  gsummptnn0fz  19865  dprdff  19893  issubdrg  20665  acsfn1p  20684  cygznlem3  21476  psdmul  22051  mptcoe1fsupp  22098  cply1coe0bi  22187  gsummoncoe1  22193  evls1fpws  22254  scmatdmat  22400  mdetdiagid  22485  mdetunilem9  22505  cpmatmcllem  22603  m2cpminvid2lem  22639  decpmatmulsumfsupp  22658  pmatcollpw1lem1  22659  pmatcollpw2lem  22662  pmatcollpwfi  22667  pm2mpf1  22684  mptcoe1matfsupp  22687  mp2pm2mplem4  22694  pm2mpmhmlem1  22703  pm2mp  22710  chpdmat  22726  chpscmat  22727  cpmidpmatlem3  22757  cayhamlem4  22773  neiptopnei  23017  cncnp  23165  isnrm2  23243  isreg2  23262  2ndcdisj  23341  islly2  23369  dislly  23382  kgen2ss  23440  ptbasfi  23466  ptclsg  23500  prdstopn  23513  txtube  23525  txlm  23533  isr0  23622  filuni  23770  alexsubALTlem3  23934  ptcmplem3  23939  ptcmplem4  23940  tsmsxplem1  24038  prdsmet  24256  metequiv2  24396  metcnpi3  24432  nmoleub  24617  rescncf  24788  cncfco  24798  evth  24856  lebnumlem3  24860  xlebnum  24862  nmoleub2lem2  25014  nmhmcn  25018  lmmcvg  25159  cmetcaulem  25186  caubl  25206  bcth3  25229  ovollb2lem  25387  ovoliunlem2  25402  ovolicc2lem3  25418  ovolicc2lem4  25419  nulmbl2  25435  volsup  25455  ioombl1lem4  25460  dyadmax  25497  vitalilem2  25508  vitalilem5  25511  mbfi1flimlem  25621  itg2seq  25641  itg2addlem  25657  itgcn  25744  limciun  25793  rolle  25892  dvfsumrlim  25936  itgsubst  25954  aannenlem1  26234  aalioulem3  26240  ulmcaulem  26301  ulmcau  26302  ulmss  26304  ulmbdd  26305  ulmcn  26306  ulmdvlem3  26309  mtest  26311  iblulm  26314  itgulm  26315  rlimcnp  26873  xrlimcnp  26876  rlimcxp  26882  o1cxp  26883  amgm  26899  lgambdd  26945  ftalem2  26982  isppw2  27023  mumullem2  27088  2sqlem6  27332  chtppilimlem2  27383  chtppilim  27384  pntrsumbnd2  27476  pntlem3  27518  nosupbnd1lem5  27622  noinfbnd1lem5  27637  noetasuplem4  27646  noetainflem4  27650  negsbdaylem  27967  mulsuniflem  28057  isperp2  28660  axeuclidlem  28907  axeuclid  28908  uhgrnbgr0nb  29299  vtxdginducedm1fi  29490  cusgrrusgr  29527  rusgrpropnb  29529  rusgrpropedg  29530  rusgrpropadjvtx  29531  upgrewlkle2  29552  wlkvtxiedg  29570  upgrwlkvtxedg  29590  uspgr2wlkeq  29591  redwlk  29616  wlkdlem2  29627  lfgrwlkprop  29631  2pthnloop  29676  upgr2pthnlp  29677  pthdlem1  29711  pthdlem2lem  29712  wlkiswwlks1  29812  wlkiswwlks2lem4  29817  wwlksm1edg  29826  wwlksnred  29837  clwwlkccatlem  29933  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  cusconngr  30135  eucrctshift  30187  2pthfrgr  30228  3cyclfrgr  30232  nmoub3i  30717  ubthlem1  30814  ubthlem3  30816  ocsh  31227  chintcli  31275  chscllem2  31582  nmopub2tALT  31853  nmfnleub2  31870  lnconi  31977  riesz1  32009  rnbra  32051  leopadd  32076  leopmuli  32077  leoptr  32081  dmdbr3  32249  dmdbr4  32250  dmdbr5  32252  mdsl0  32254  mdsymlem6  32352  cdj1i  32377  acunirnmpt  32602  xrge0infss  32703  isdrng4  33234  elrspunidl  33365  cmppcmp  33825  zarclsiin  33838  lmxrge0  33919  ftc2re  34566  cvmlift2lem12  35291  opnrebl2  36299  neibastop1  36337  neibastop2lem  36338  neibastop3  36340  finixpnum  37589  lindsenlbs  37599  matunitlindflem1  37600  matunitlindflem2  37601  ptrecube  37604  poimirlem26  37630  poimirlem27  37631  poimirlem29  37633  poimirlem30  37634  poimir  37637  heicant  37639  itg2addnclem  37655  itg2addnclem3  37657  itg2addnc  37658  filbcmb  37724  nninfnub  37735  geomcau  37743  sstotbnd2  37758  isbndx  37766  prdsbnd  37777  heibor1lem  37793  heiborlem1  37795  heibor  37805  rrncmslem  37816  intidl  38013  pclclN  39874  lauteq  40078  ltrnid  40118  mapdh9a  41772  primrootscoprmpow  42076  sticksstones3  42125  aks5lem5a  42168  aks5lem6  42169  fltaccoprm  42617  fltabcoprm  42619  flt4lem5  42627  elrfirn2  42673  isnacs3  42687  rencldnfilem  42797  kelac1  43040  naddgeoa  43371  neik0pk1imk0  44024  cvgdvgrat  44290  neglimc  45632  limsupub  45689  limsuppnflem  45695  limsupre3lem  45717  limsupvaluz2  45723  supcnvlimsup  45725  climuzlem  45728  liminfval2  45753  limsupgtlem  45762  liminflelimsupuz  45770  liminflimsupclim  45792  xlimpnfxnegmnf  45799  liminflimsupxrre  45802  xlimmnfv  45819  xlimpnfv  45823  stoweidlem7  45992  fourierdlem73  46164  sge0isum  46412  meaiuninc3v  46469  preimageiingt  46705  preimaleiinlt  46706  smflimlem3  46758  smflimlem4  46759  cfsetsnfsetfo  47048  2reu8i  47101  iccpartres  47406  uhgrimisgrgric  47919  grlictr  48003  clnbgr3stgrgrlim  48007  clnbgr3stgrgrlic  48008  upwlkwlk  48127  upgrwlkupwlk  48128  copisnmnd  48157  2zrngnmlid2  48245  ply1mulgsumlem1  48375  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  snlindsntor  48460  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  iinfsubc  49047