Theorem ralimdva 3177

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

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

This theorem is used by:  ralimdv  3179  ralimdvva  3212  wereu2  5651  frpomin  6349  fveqressseq  7087  f1mpt  7272  isores3  7350  caofrss  7739  caoftrn  7741  sorpssuni  7755  sorpssint  7756  onint  7811  xpord3inddlem  8181  smogt  8386  fisupg  9290  ixpfi2  9350  fissuni  9357  indexfi  9360  fiinfg  9503  wemaplem2  9551  rankonidlem  9848  ac5num  10125  acni2  10135  acndom2  10143  alephle  10177  dfac5  10217  cfsmolem  10358  isf34lem7  10467  isf34lem6  10468  fin1a2s  10502  acncc  10528  ttukeylem6  10602  fpwwe2lem7  10732  gchina  10794  inar1  10870  tskord  10875  grudomon  10912  grur1a  10914  dedekind  11483  fimaxre  12271  fiminre  12274  uzwo  13048  xrsupsslem  13447  xrinfmsslem  13448  fsuppmapnn0fiub0  14146  rexanre  15526  rexuz3  15528  rexico  15533  cau3lem  15534  limsupval2  15659  rlim2lt  15676  rlim3  15677  lo1bdd2  15703  lo1bddrp  15704  o1lo1  15716  climrlim2  15726  2clim  15751  o1co  15765  rlimcn1  15767  rlimcn3  15769  climcn1  15771  climcn2  15772  subcn2  15774  o1of2  15792  rlimo1  15796  o1rlimmul  15798  lo1add  15806  lo1mul  15807  climsqz  15820  climsqz2  15821  rlimsqzlem  15828  lo1le  15831  climbdd  15851  caucvgrlem  15852  caucvgrlem2  15854  caurcvg2  15857  iseralt  15864  cvgcmp  15995  cvgcmpce  15997  gcdcllem1  16681  absproddvds  16804  coprmprod  16848  coprmproddvdslem  16849  pcfac  17089  pockthg  17096  infpnlem1  17100  prmreclem2  17107  prmreclem3  17108  vdwlem11  17181  vdwlem13  17183  vdwnnlem3  17187  isacs2  17839  acsfn1  17847  acsfn2  17849  catpropd  17895  drsdirfi  18491  ipodrsima  18727  isacs5  18734  mrelatglb  18746  mrelatlub  18748  isgrpinv  19216  dfgrp3e  19262  issubg4  19368  gsmsymgreqlem2  19657  finodsubmsubg  19793  gexdvds  19810  gexcl3  19813  sylow2blem3  19848  cyggeninv  20109  gsummptnn0fz  20212  dprdff  20240  isdrng4  21004  issubdrg  21049  acsfn1p  21068  cygznlem3  21887  lindsenlbs  22169  psdmul  22499  mptcoe1fsupp  22545  cply1coe0bi  22632  gsummoncoe1  22638  evls1fpws  22699  scmatdmat  22842  mdetdiagid  22927  mdetunilem9  22947  matunitlindflem1  23006  matunitlindflem2  23007  cpmatmcllem  23048  m2cpminvid2lem  23084  decpmatmulsumfsupp  23103  pmatcollpw1lem1  23104  pmatcollpw2lem  23107  pmatcollpwfi  23112  pm2mpf1  23129  mptcoe1matfsupp  23132  mp2pm2mplem4  23139  pm2mpmhmlem1  23148  pm2mp  23155  chpdmat  23171  chpscmat  23172  cpmidpmatlem3  23202  cayhamlem4  23218  neiptopnei  23462  cncnp  23610  isnrm2  23688  isreg2  23707  2ndcdisj  23787  islly2  23815  dislly  23828  kgen2ss  23886  ptbasfi  23912  ptclsg  23946  prdstopn  23959  txtube  23971  txlm  23979  isr0  24068  filuni  24216  alexsubALTlem3  24380  ptcmplem3  24385  ptcmplem4  24386  tsmsxplem1  24484  prdsmet  24701  metequiv2  24841  metcnpi3  24877  nmoleub  25062  rescncf  25230  cncfco  25240  evth  25292  lebnumlem3  25296  xlebnum  25298  nmoleub2lem2  25449  nmhmcn  25453  lmmcvg  25594  cmetcaulem  25621  caubl  25641  bcth3  25664  ovollb2lem  25821  ovoliunlem2  25836  ovolicc2lem3  25852  ovolicc2lem4  25853  nulmbl2  25869  volsup  25889  ioombl1lem4  25894  dyadmax  25931  vitalilem2  25942  vitalilem5  25945  mbfi1flimlem  26055  itg2seq  26075  itg2addlem  26091  itgcn  26177  limciun  26226  rolle  26322  dvfsumrlim  26363  itgsubst  26381  aannenlem1  26667  aalioulem3  26673  ulmcaulem  26733  ulmcau  26734  ulmss  26736  ulmbdd  26737  ulmcn  26738  ulmdvlem3  26741  mtest  26743  iblulm  26746  itgulm  26747  rlimcnp  27305  xrlimcnp  27308  rlimcxp  27313  o1cxp  27314  amgm  27330  lgambdd  27376  ftalem2  27413  isppw2  27454  mumullem2  27519  2sqlem6  27762  chtppilimlem2  27813  chtppilim  27814  pntrsumbnd2  27906  pntlem3  27948  fltaccoprm  27984  fltabcoprm  27986  flt4lem5  27992  nosupbnd1lem5  28081  noinfbnd1lem5  28096  noetasuplem4  28105  noetainflem4  28109  negbdaylem  28454  mulsuniflem  28547  elreno2  28893  isperp2  29202  axeuclidlem  29552  axeuclid  29553  uhgrnbgr0nb  29947  vtxdginducedm1fi  30137  cusgrrusgr  30174  rusgrpropnb  30176  rusgrpropedg  30177  rusgrpropadjvtx  30178  upgrewlkle2  30199  wlkvtxiedg  30217  upgrwlkvtxedg  30237  uspgr2wlkeq  30238  redwlk  30263  wlkdlem2  30274  lfgrwlkprop  30282  2pthnloop  30329  upgr2pthnlp  30330  pthdlem1  30364  pthdlem2lem  30365  wlkiswwlks1  30468  wlkiswwlks2lem4  30473  wwlksm1edg  30482  wwlksnred  30493  clwwlkccatlem  30592  clwlkclwwlklem2a  30601  clwlkclwwlklem2  30603  cusconngr  30804  eucrctshift  30856  2pthfrgr  30897  3cyclfrgr  30901  nmoub3i  31387  ubthlem1  31484  ubthlem3  31486  ocsh  31897  chintcli  31945  chscllem2  32252  nmopub2tALT  32523  nmfnleub2  32540  lnconi  32647  riesz1  32679  rnbra  32721  leopadd  32746  leopmuli  32747  leoptr  32751  dmdbr3  32919  dmdbr4  32920  dmdbr5  32922  mdsl0  32924  mdsymlem6  33022  cdj1i  33047  acunirnmpt  33307  xrge0infss  33405  elrspunidl  34031  dflring2  34078  cmppcmp  34543  zarclsiin  34556  lmxrge0  34637  ftc2re  35280  cvmlift2lem12  36200  nmulrid  37073  opnrebl2  37236  neibastop1  37274  neibastop2lem  37275  neibastop3  37277  finixpnum  38668  ptrecube  38678  poimirlem26  38704  poimirlem27  38705  poimirlem29  38707  poimirlem30  38708  poimir  38711  heicant  38713  itg2addnclem  38729  itg2addnclem3  38731  itg2addnc  38732  filbcmb  38814  nninfnub  38825  geomcau  38833  sstotbnd2  38848  isbndx  38856  prdsbnd  38867  heibor1lem  38883  heiborlem1  38885  heibor  38895  rrncmslem  38906  intidl  39103  pclclN  41088  lauteq  41292  ltrnid  41332  mapdh9a  42986  primrootscoprmpow  43289  sticksstones3  43338  aks5lem5a  43381  aks5lem6  43382  elrfirn2  43847  isnacs3  43861  rencldnfilem  43967  kelac1  44205  naddgeoa  44536  neik0pk1imk0  45187  cvgdvgrat  45437  neglimc  46796  limsupub  46853  limsuppnflem  46859  limsupre3lem  46881  limsupvaluz2  46887  supcnvlimsup  46889  climuzlem  46892  liminfval2  46917  limsupgtlem  46926  liminflelimsupuz  46934  liminflimsupclim  46956  xlimpnfxnegmnf  46963  liminflimsupxrre  46966  xlimmnfv  46983  xlimpnfv  46987  stoweidlem7  47156  fourierdlem73  47328  sge0isum  47576  meaiuninc3v  47633  preimageiingt  47869  preimaleiinlt  47870  smflimlem3  47922  smflimlem4  47923  cfsetsnfsetfo  48269  2reu8i  48323  iccpartres  48639  uhgrimisgrgric  49168  grlictr  49252  clnbgr3stgrgrlim  49256  clnbgr3stgrgrlic  49257  upwlkwlk  49376  upgrwlkupwlk  49377  copisnmnd  49405  2zrngnmlid2  49493  ply1mulgsumlem1  49637  ply1mulgsumlem3  49639  ply1mulgsumlem4  49640  snlindsntor  49722  eenglngeehlnmlem1  49989  eenglngeehlnmlem2  49990  iinfsubc  50311