Theorem ralimdva 2945

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 449	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralimdv2 2944	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  ralimdv  2946  ralimdvva  2947  wereu2  5035  fveqressseq  6263  f1mpt  6419  isores3  6485  caofrss  6828  caoftrn  6830  sorpssuni  6844  sorpssint  6845  onint  6887  smogt  7351  fisupg  8093  ixpfi2  8147  fissuni  8154  indexfi  8157  fiinfg  8288  wemaplem2  8335  rankonidlem  8574  ac5num  8742  acni2  8752  acndom2  8760  alephle  8794  dfac5  8834  cfsmolem  8975  isf34lem7  9084  isf34lem6  9085  fin1a2s  9119  acncc  9145  ttukeylem6  9219  fpwwe2lem8  9338  gchina  9400  inar1  9476  tskord  9481  grudomon  9518  grur1a  9520  dedekind  10079  fimaxre  10847  uzwo  11627  xrsupsslem  12009  xrinfmsslem  12010  fsuppmapnn0fiub0  12655  rexanre  13934  rexuz3  13936  rexico  13941  cau3lem  13942  limsupval2  14059  rlim2lt  14076  rlim3  14077  lo1bdd2  14103  lo1bddrp  14104  o1lo1  14116  climrlim2  14126  2clim  14151  o1co  14165  rlimcn1  14167  rlimcn2  14169  climcn1  14170  climcn2  14171  subcn2  14173  o1of2  14191  rlimo1  14195  o1rlimmul  14197  lo1add  14205  lo1mul  14206  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  lo1le  14230  climbdd  14250  caucvgrlem  14251  caucvgrlem2  14253  caurcvg2  14256  iseralt  14263  cvgcmp  14389  cvgcmpce  14391  gcdcllem1  15059  absproddvds  15168  coprmprod  15213  coprmproddvdslem  15214  pcfac  15441  pockthg  15448  infpnlem1  15452  prmreclem2  15459  prmreclem3  15460  vdwlem11  15533  vdwlem13  15535  vdwnnlem3  15539  isacs2  16137  acsfn1  16145  acsfn2  16147  catpropd  16192  drsdirfi  16761  ipodrsima  16988  isacs5  16995  mrelatglb  17007  mrelatlub  17009  isgrpinv  17295  dfgrp3e  17338  issubg4  17436  gsmsymgreqlem2  17674  gexdvds  17822  gexcl3  17825  sylow2blem3  17860  cyggeninv  18108  gsummptnn0fz  18205  dprdff  18234  issubdrg  18628  mptcoe1fsupp  19406  cply1coe0bi  19491  gsummoncoe1  19495  cygznlem3  19737  scmatdmat  20140  mdetdiagid  20225  mdetunilem9  20245  cpmatmcllem  20342  m2cpminvid2lem  20378  decpmatmulsumfsupp  20397  pmatcollpw1lem1  20398  pmatcollpw2lem  20401  pmatcollpwfi  20406  pm2mpf1  20423  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  pm2mpmhmlem1  20442  pm2mp  20449  chpdmat  20465  chpscmat  20466  cpmidpmatlem3  20496  cayhamlem4  20512  neiptopnei  20746  cncnp  20894  isnrm2  20972  isreg2  20991  2ndcdisj  21069  islly2  21097  dislly  21110  kgen2ss  21168  ptbasfi  21194  ptclsg  21228  prdstopn  21241  txtube  21253  txlm  21261  isr0  21350  filuni  21499  alexsubALTlem3  21663  ptcmplem3  21668  ptcmplem4  21669  tsmsxplem1  21766  prdsmet  21985  metequiv2  22125  metcnpi3  22161  nmoleub  22345  rescncf  22508  cncfco  22518  evth  22566  lebnumlem3  22570  xlebnum  22572  nmoleub2lem2  22724  nmhmcn  22728  lmmcvg  22867  cmetcaulem  22894  caubl  22914  bcth3  22936  ovollb2lem  23063  ovoliunlem2  23078  ovolicc2lem3  23094  ovolicc2lem4  23095  nulmbl2  23111  volsup  23131  ioombl1lem4  23136  dyadmax  23172  vitalilem2  23184  vitalilem5  23187  mbfi1flimlem  23295  itg2seq  23315  itg2addlem  23331  itgcn  23415  limciun  23464  rolle  23557  dvfsumrlim  23598  itgsubst  23616  aannenlem1  23887  aalioulem3  23893  ulmcaulem  23952  ulmcau  23953  ulmss  23955  ulmbdd  23956  ulmcn  23957  ulmdvlem3  23960  mtest  23962  iblulm  23965  itgulm  23966  rlimcnp  24492  xrlimcnp  24495  rlimcxp  24500  o1cxp  24501  amgm  24517  lgambdd  24563  ftalem2  24600  isppw2  24641  mumullem2  24706  2sqlem6  24948  chtppilimlem2  24963  chtppilim  24964  pntrsumbnd2  25056  pntlem3  25098  isperp2  25410  axeuclidlem  25642  axeuclid  25643  cusgrares  26001  edgwlk  26059  usgrwlknloop  26093  redwlk  26136  cusconngra  26204  wlkiswwlk1  26218  wlkiswwlk2lem4  26222  usg2wlkeq  26236  wwlknred  26251  wwlkm1edg  26263  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  usgravd00  26446  cusgraisrusgra  26465  rusgraprop2  26469  rusgraprop3  26470  frisusgranb  26524  2pthfrgrarn  26536  2pthfrgrarn2  26537  2pthfrgra  26538  3cyclfrgra  26542  frgrancvvdeq  26569  frgrancvvdgeq  26570  nmoub3i  27012  ubthlem1  27110  ubthlem3  27112  ocsh  27526  chintcli  27574  chscllem2  27881  nmopub2tALT  28152  nmfnleub2  28169  lnconi  28276  riesz1  28308  rnbra  28350  leopadd  28375  leopmuli  28376  leoptr  28380  dmdbr3  28548  dmdbr4  28549  dmdbr5  28551  mdsl0  28553  mdsymlem6  28651  cdj1i  28676  acunirnmpt  28841  xrge0infss  28915  cmppcmp  29253  lmxrge0  29326  cvmlift2lem12  30550  opnrebl2  31486  neibastop1  31524  neibastop2lem  31525  neibastop3  31527  finixpnum  32564  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  ptrecube  32579  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  poimir  32612  heicant  32614  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  filbcmb  32705  nninfnub  32717  geomcau  32725  sstotbnd2  32743  isbndx  32751  prdsbnd  32762  heibor1lem  32778  heiborlem1  32780  heibor  32790  rrncmslem  32801  intidl  32998  pclclN  34195  lauteq  34399  ltrnid  34439  mapdh9a  36097  elrfirn2  36277  isnacs3  36291  rencldnfilem  36402  kelac1  36651  acsfn1p  36788  neik0pk1imk0  37365  cvgdvgrat  37534  neglimc  38714  stoweidlem7  38900  fourierdlem73  39072  sge0isum  39320  preimageiingt  39607  preimaleiinlt  39608  smflimlem3  39659  smflimlem4  39660  iccpartres  39956  uhgrnbgr0nb  40576  cusgrrusgr  40781  rusgrpropnb  40783  rusgrpropedg  40784  rusgrpropadjvtx  40785  upgrewlkle2  40808  1wlkvtxiedg  40829  wlk1wlk  40846  upgr1wlkwlk  40847  upgr1wlkvtxedg  40853  uspgr2wlkeq  40854  red1wlk  40881  1wlkdlem2  40892  lfgrwlkprop  40896  2pthnloop  40937  upgr2pthnlp  40938  pthdlem1  40972  pthdlem2lem  40973  1wlkiswwlks1  41064  1wlkiswwlks2lem4  41069  wwlksm1edg  41078  wwlksnred  41098  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  cusconngr  41358  eucrctshift  41411  2pthfrgr  41454  3cyclfrgr  41458  copisnmnd  41599  2zrngnmlid2  41741  ply1mulgsumlem1  41968  ply1mulgsumlem3  41970  ply1mulgsumlem4  41971  snlindsntor  42054