Theorem ralimdv 3146

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1811). (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3144	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3048

This theorem is referenced by:  r19.21v  3157  ralimdvv  3181  ss2ralv  4000  poss  5524  sess1  5579  sess2  5580  riinint  5910  iinpreima  7002  dffo4  7036  dffo5  7037  isoini2  7273  tfindsg  7791  el2mpocsbcl  8015  xpord3inddlem  8084  iiner  8713  xpf1o  9052  dffi3  9315  brwdom3  9468  xpwdomg  9471  ttrclss  9610  bndrank  9734  cfub  10140  cff1  10149  cfflb  10150  cfslb2n  10159  cofsmo  10160  cfcoflem  10163  pwcfsdom  10474  fpwwe2lem12  10533  inawinalem  10580  grupr  10688  fsequb  13882  cau3lem  15262  caubnd2  15265  caubnd  15266  rlim2lt  15404  rlim3  15405  climshftlem  15481  climcau  15578  caucvgb  15587  serf0  15588  modfsummods  15700  cvgcmp  15723  mreriincl  17500  acsfn1c  17568  resspos  18335  resstos  18336  chnrss  18521  islss4  20895  riinopn  22823  fiinbas  22867  baspartn  22869  isclo2  23003  lmcls  23217  lmcnp  23219  isnrm3  23274  1stcelcls  23376  llyss  23394  nllyss  23395  ptpjpre1  23486  txlly  23551  txnlly  23552  tx1stc  23565  xkococnlem  23574  fbunfip  23784  filssufilg  23826  cnpflf2  23915  fcfnei  23950  isucn2  24193  rescncf  24817  lebnum  24890  cfilss  25197  fgcfil  25198  iscau4  25206  cmetcaulem  25215  caussi  25224  ovolunlem1  25425  ulmclm  26323  ulmcaulem  26330  ulmcau  26331  ulmss  26333  rlimcnp  26902  cxploglim  26915  2sqreunnlem2  27393  pntlemp  27548  nosupno  27642  nosupres  27646  noinfno  27657  noinfres  27661  sssslt2  27737  madebdayim  27833  madebdaylemold  27843  axcontlem4  28945  ewlkle  29584  uspgr2wlkeq  29624  umgrwlknloop  29627  wlkiswwlksupgr2  29855  3cyclfrgrrn2  30267  nmlnoubi  30776  lnon0  30778  disjpreima  32564  submarchi  33155  prmidl2  33406  crefss  33862  r1filimi  35114  iccllysconn  35294  cvmlift2lem1  35346  dmopab3rexdif  35449  ss2mcls  35612  mclsax  35613  isinf2  37449  poimirlem25  37695  poimirlem27  37697  upixp  37779  caushft  37811  sstotbnd3  37826  totbndss  37827  unichnidl  38081  ispridl2  38088  elrfirn2  42799  mzpsubst  42851  eluzrabdioph  42909  neik0pk1imk0  44150  mnuop3d  44374  ismnushort  44404  pwclaxpow  45087  limsupub  45812  limsupre3lem  45840  climuzlem  45851  xlimbr  45935  fourierdlem103  46317  fourierdlem104  46318  qndenserrnbllem  46402  2reuimp  47225  ralralimp  47388