Theorem ralimdv 3156

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  r19.21v  3167  ss2ralv  4034  poss  5574  sess1  5630  sess2  5631  riinint  5962  iinpreima  7069  dffo4  7103  dffo5  7104  isoini2  7341  tfindsg  7864  el2mpocsbcl  8092  xpord3inddlem  8161  iiner  8811  xpf1o  9161  dffi3  9453  brwdom3  9604  xpwdomg  9607  ttrclss  9742  bndrank  9863  cfub  10271  cff1  10280  cfflb  10281  cfslb2n  10290  cofsmo  10291  cfcoflem  10294  pwcfsdom  10605  fpwwe2lem12  10664  inawinalem  10711  grupr  10819  fsequb  13998  cau3lem  15376  caubnd2  15379  caubnd  15380  rlim2lt  15516  rlim3  15517  climshftlem  15593  climcau  15690  caucvgb  15699  serf0  15700  modfsummods  15812  cvgcmp  15835  mreriincl  17613  acsfn1c  17677  islss4  20929  riinopn  22863  fiinbas  22907  baspartn  22909  isclo2  23043  lmcls  23257  lmcnp  23259  isnrm3  23314  1stcelcls  23416  llyss  23434  nllyss  23435  ptpjpre1  23526  txlly  23591  txnlly  23592  tx1stc  23605  xkococnlem  23614  fbunfip  23824  filssufilg  23866  cnpflf2  23955  fcfnei  23990  isucn2  24234  rescncf  24860  lebnum  24933  cfilss  25241  fgcfil  25242  iscau4  25250  cmetcaulem  25259  caussi  25268  ovolunlem1  25469  ulmclm  26367  ulmcaulem  26374  ulmcau  26375  ulmss  26377  rlimcnp  26945  cxploglim  26958  2sqreunnlem2  27436  pntlemp  27591  nosupno  27685  nosupres  27689  noinfno  27700  noinfres  27704  sssslt2  27778  madebdayim  27863  madebdaylemold  27873  axcontlem4  28913  ewlkle  29552  uspgr2wlkeq  29593  umgrwlknloop  29596  wlkiswwlksupgr2  29826  3cyclfrgrrn2  30235  nmlnoubi  30744  lnon0  30746  disjpreima  32533  resspos  32900  resstos  32901  submarchi  33137  prmidl2  33409  crefss  33823  iccllysconn  35230  cvmlift2lem1  35282  dmopab3rexdif  35385  ss2mcls  35548  mclsax  35549  isinf2  37381  poimirlem25  37627  poimirlem27  37629  upixp  37711  caushft  37743  sstotbnd3  37758  totbndss  37759  unichnidl  38013  ispridl2  38020  elrfirn2  42685  mzpsubst  42737  eluzrabdioph  42795  neik0pk1imk0  44037  mnuop3d  44262  ismnushort  44292  pwclaxpow  44973  limsupub  45691  limsupre3lem  45719  climuzlem  45730  xlimbr  45814  fourierdlem103  46196  fourierdlem104  46197  qndenserrnbllem  46281  2reuimp  47100  ralralimp  47263