Theorem ralimdv 3152

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 3150	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

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

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 3053

This theorem is referenced by:  r19.21v  3163  ralimdvv  3187  ss2ralv  4006  poss  5542  sess1  5597  sess2  5598  riinint  5929  iinpreima  7023  dffo4  7057  dffo5  7058  isoini2  7295  tfindsg  7813  el2mpocsbcl  8037  xpord3inddlem  8106  iiner  8738  xpf1o  9079  dffi3  9346  brwdom3  9499  xpwdomg  9502  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  13910  cau3lem  15290  caubnd2  15293  caubnd  15294  rlim2lt  15432  rlim3  15433  climshftlem  15509  climcau  15606  caucvgb  15615  serf0  15616  modfsummods  15728  cvgcmp  15751  mreriincl  17529  acsfn1c  17597  resspos  18364  resstos  18365  chnrss  18550  islss4  20928  riinopn  22867  fiinbas  22911  baspartn  22913  isclo2  23047  lmcls  23261  lmcnp  23263  isnrm3  23318  1stcelcls  23420  llyss  23438  nllyss  23439  ptpjpre1  23530  txlly  23595  txnlly  23596  tx1stc  23609  xkococnlem  23618  fbunfip  23828  filssufilg  23870  cnpflf2  23959  fcfnei  23994  isucn2  24237  rescncf  24861  lebnum  24934  cfilss  25241  fgcfil  25242  iscau4  25250  cmetcaulem  25259  caussi  25268  ovolunlem1  25469  ulmclm  26367  ulmcaulem  26374  ulmcau  26375  ulmss  26377  rlimcnp  26946  cxploglim  26959  2sqreunnlem2  27437  pntlemp  27592  nosupno  27686  nosupres  27690  noinfno  27701  noinfres  27705  ssslts2  27785  madebdayim  27899  madebdaylemold  27909  axcontlem4  29056  ewlkle  29695  uspgr2wlkeq  29735  umgrwlknloop  29738  wlkiswwlksupgr2  29966  3cyclfrgrrn2  30378  nmlnoubi  30888  lnon0  30890  disjpreima  32675  submarchi  33284  prmidl2  33538  crefss  34031  r1filimi  35284  iccllysconn  35470  cvmlift2lem1  35522  dmopab3rexdif  35625  ss2mcls  35788  mclsax  35789  isinf2  37664  poimirlem25  37900  poimirlem27  37902  upixp  37984  caushft  38016  sstotbnd3  38031  totbndss  38032  unichnidl  38286  ispridl2  38293  elrfirn2  43057  mzpsubst  43109  eluzrabdioph  43167  neik0pk1imk0  44407  mnuop3d  44631  ismnushort  44661  pwclaxpow  45344  limsupub  46066  limsupre3lem  46094  climuzlem  46105  xlimbr  46189  fourierdlem103  46571  fourierdlem104  46572  qndenserrnbllem  46656  2reuimp  47479  ralralimp  47642