Theorem ralimdv 3153

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1817). (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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3151	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3054

This theorem is referenced by:  r19.21v  3164  ralimdvv  3188  ss2ralv  3985  poss  5528  sess1  5583  sess2  5584  riinint  5914  iinpreima  7010  dffo4  7044  dffo5  7045  isoini2  7283  tfindsg  7801  el2mpocsbcl  8024  xpord3inddlem  8094  iiner  8726  xpf1o  9067  dffi3  9334  brwdom3  9487  xpwdomg  9490  ttrclss  9632  bndrank  9756  cfub  10162  cff1  10171  cfflb  10172  cfslb2n  10181  cofsmo  10182  cfcoflem  10185  pwcfsdom  10497  fpwwe2lem12  10556  inawinalem  10603  grupr  10711  fsequb  13928  cau3lem  15308  caubnd2  15311  caubnd  15312  rlim2lt  15450  rlim3  15451  climshftlem  15527  climcau  15624  caucvgb  15633  serf0  15634  modfsummods  15747  cvgcmp  15770  mreriincl  17551  acsfn1c  17619  resspos  18386  resstos  18387  chnrss  18572  islss4  20952  riinopn  22891  fiinbas  22935  baspartn  22937  isclo2  23071  lmcls  23285  lmcnp  23287  isnrm3  23342  1stcelcls  23444  llyss  23462  nllyss  23463  ptpjpre1  23554  txlly  23619  txnlly  23620  tx1stc  23633  xkococnlem  23642  fbunfip  23852  filssufilg  23894  cnpflf2  23983  fcfnei  24018  isucn2  24261  rescncf  24882  lebnum  24949  cfilss  25255  fgcfil  25256  iscau4  25264  cmetcaulem  25273  caussi  25282  ovolunlem1  25482  ulmclm  26370  ulmcaulem  26377  ulmcau  26378  ulmss  26380  rlimcnp  26947  cxploglim  26959  2sqreunnlem2  27436  pntlemp  27591  nosupno  27685  nosupres  27689  noinfno  27700  noinfres  27704  ssslts2  27784  madebdayim  27898  madebdaylemold  27908  axcontlem4  29054  ewlkle  29692  uspgr2wlkeq  29732  umgrwlknloop  29735  wlkiswwlksupgr2  29963  3cyclfrgrrn2  30375  nmlnoubi  30885  lnon0  30887  disjpreima  32673  submarchi  33267  prmidl2  33524  crefss  34033  r1filimi  35284  iccllysconn  35478  cvmlift2lem1  35530  dmopab3rexdif  35633  ss2mcls  35796  mclsax  35797  dfttc4lem2  36757  isinf2  37767  poimirlem25  38012  poimirlem27  38014  upixp  38096  caushft  38128  sstotbnd3  38143  totbndss  38144  unichnidl  38398  ispridl2  38405  elrfirn2  43145  mzpsubst  43197  eluzrabdioph  43251  neik0pk1imk0  44491  mnuop3d  44715  ismnushort  44745  pwclaxpow  45428  limsupub  46147  limsupre3lem  46175  climuzlem  46186  xlimbr  46270  fourierdlem103  46652  fourierdlem104  46653  qndenserrnbllem  46737  2reuimp  47578  ralralimp  47741