Theorem ralimdv 3151

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  r19.21v  3162  ralimdvv  3186  ss2ralv  3992  poss  5541  sess1  5596  sess2  5597  riinint  5927  iinpreima  7021  dffo4  7055  dffo5  7056  isoini2  7294  tfindsg  7812  el2mpocsbcl  8035  xpord3inddlem  8104  iiner  8736  xpf1o  9077  dffi3  9344  brwdom3  9497  xpwdomg  9500  ttrclss  9641  bndrank  9765  cfub  10171  cff1  10180  cfflb  10181  cfslb2n  10190  cofsmo  10191  cfcoflem  10194  pwcfsdom  10506  fpwwe2lem12  10565  inawinalem  10612  grupr  10720  fsequb  13937  cau3lem  15317  caubnd2  15320  caubnd  15321  rlim2lt  15459  rlim3  15460  climshftlem  15536  climcau  15633  caucvgb  15642  serf0  15643  modfsummods  15756  cvgcmp  15779  mreriincl  17560  acsfn1c  17628  resspos  18395  resstos  18396  chnrss  18581  islss4  20957  riinopn  22873  fiinbas  22917  baspartn  22919  isclo2  23053  lmcls  23267  lmcnp  23269  isnrm3  23324  1stcelcls  23426  llyss  23444  nllyss  23445  ptpjpre1  23536  txlly  23601  txnlly  23602  tx1stc  23615  xkococnlem  23624  fbunfip  23834  filssufilg  23876  cnpflf2  23965  fcfnei  24000  isucn2  24243  rescncf  24864  lebnum  24931  cfilss  25237  fgcfil  25238  iscau4  25246  cmetcaulem  25255  caussi  25264  ovolunlem1  25464  ulmclm  26352  ulmcaulem  26359  ulmcau  26360  ulmss  26362  rlimcnp  26929  cxploglim  26941  2sqreunnlem2  27418  pntlemp  27573  nosupno  27667  nosupres  27671  noinfno  27682  noinfres  27686  ssslts2  27766  madebdayim  27880  madebdaylemold  27890  axcontlem4  29036  ewlkle  29674  uspgr2wlkeq  29714  umgrwlknloop  29717  wlkiswwlksupgr2  29945  3cyclfrgrrn2  30357  nmlnoubi  30867  lnon0  30869  disjpreima  32654  submarchi  33247  prmidl2  33501  crefss  33993  r1filimi  35246  iccllysconn  35432  cvmlift2lem1  35484  dmopab3rexdif  35587  ss2mcls  35750  mclsax  35751  dfttc4lem2  36711  isinf2  37721  poimirlem25  37966  poimirlem27  37968  upixp  38050  caushft  38082  sstotbnd3  38097  totbndss  38098  unichnidl  38352  ispridl2  38359  elrfirn2  43128  mzpsubst  43180  eluzrabdioph  43234  neik0pk1imk0  44474  mnuop3d  44698  ismnushort  44728  pwclaxpow  45411  limsupub  46132  limsupre3lem  46160  climuzlem  46171  xlimbr  46255  fourierdlem103  46637  fourierdlem104  46638  qndenserrnbllem  46722  2reuimp  47563  ralralimp  47726