Theorem ralimdv 3154

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  r19.21v  3165  ss2ralv  4029  poss  5563  sess1  5619  sess2  5620  riinint  5951  iinpreima  7058  dffo4  7092  dffo5  7093  isoini2  7331  tfindsg  7854  el2mpocsbcl  8082  xpord3inddlem  8151  iiner  8801  xpf1o  9151  dffi3  9441  brwdom3  9594  xpwdomg  9597  ttrclss  9732  bndrank  9853  cfub  10261  cff1  10270  cfflb  10271  cfslb2n  10280  cofsmo  10281  cfcoflem  10284  pwcfsdom  10595  fpwwe2lem12  10654  inawinalem  10701  grupr  10809  fsequb  13991  cau3lem  15371  caubnd2  15374  caubnd  15375  rlim2lt  15511  rlim3  15512  climshftlem  15588  climcau  15685  caucvgb  15694  serf0  15695  modfsummods  15807  cvgcmp  15830  mreriincl  17608  acsfn1c  17672  islss4  20917  riinopn  22844  fiinbas  22888  baspartn  22890  isclo2  23024  lmcls  23238  lmcnp  23240  isnrm3  23295  1stcelcls  23397  llyss  23415  nllyss  23416  ptpjpre1  23507  txlly  23572  txnlly  23573  tx1stc  23586  xkococnlem  23595  fbunfip  23805  filssufilg  23847  cnpflf2  23936  fcfnei  23971  isucn2  24215  rescncf  24839  lebnum  24912  cfilss  25220  fgcfil  25221  iscau4  25229  cmetcaulem  25238  caussi  25247  ovolunlem1  25448  ulmclm  26346  ulmcaulem  26353  ulmcau  26354  ulmss  26356  rlimcnp  26925  cxploglim  26938  2sqreunnlem2  27416  pntlemp  27571  nosupno  27665  nosupres  27669  noinfno  27680  noinfres  27684  sssslt2  27758  madebdayim  27843  madebdaylemold  27853  axcontlem4  28892  ewlkle  29531  uspgr2wlkeq  29572  umgrwlknloop  29575  wlkiswwlksupgr2  29805  3cyclfrgrrn2  30214  nmlnoubi  30723  lnon0  30725  disjpreima  32511  resspos  32892  resstos  32893  submarchi  33130  prmidl2  33402  crefss  33826  iccllysconn  35218  cvmlift2lem1  35270  dmopab3rexdif  35373  ss2mcls  35536  mclsax  35537  isinf2  37369  poimirlem25  37615  poimirlem27  37617  upixp  37699  caushft  37731  sstotbnd3  37746  totbndss  37747  unichnidl  38001  ispridl2  38008  elrfirn2  42666  mzpsubst  42718  eluzrabdioph  42776  neik0pk1imk0  44018  mnuop3d  44243  ismnushort  44273  pwclaxpow  44957  limsupub  45681  limsupre3lem  45709  climuzlem  45720  xlimbr  45804  fourierdlem103  46186  fourierdlem104  46187  qndenserrnbllem  46271  2reuimp  47092  ralralimp  47255