Theorem ralimdv 2992

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

Syntax hints:   → wi 4   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946

This theorem is referenced by:  poss  5066  sess1  5111  sess2  5112  riinint  5414  iinpreima  6385  dffo4  6415  dffo5  6416  isoini2  6629  tfindsg  7102  el2mpt2csbcl  7295  iiner  7862  xpf1o  8163  dffi3  8378  brwdom3  8528  xpwdomg  8531  bndrank  8742  cfub  9109  cff1  9118  cfflb  9119  cfslb2n  9128  cofsmo  9129  cfcoflem  9132  pwcfsdom  9443  fpwwe2lem13  9502  inawinalem  9549  grupr  9657  fsequb  12814  cau3lem  14138  caubnd2  14141  caubnd  14142  rlim2lt  14272  rlim3  14273  climshftlem  14349  isercolllem1  14439  climcau  14445  caucvgb  14454  serf0  14455  modfsummods  14569  cvgcmp  14592  mreriincl  16305  acsfn1c  16370  islss4  19010  riinopn  20761  fiinbas  20804  baspartn  20806  isclo2  20940  lmcls  21154  lmcnp  21156  isnrm3  21211  1stcelcls  21312  llyss  21330  nllyss  21331  ptpjpre1  21422  txlly  21487  txnlly  21488  tx1stc  21501  xkococnlem  21510  fbunfip  21720  filssufilg  21762  cnpflf2  21851  fcfnei  21886  isucn2  22130  rescncf  22747  lebnum  22810  cfilss  23114  fgcfil  23115  iscau4  23123  cmetcaulem  23132  cfilres  23140  caussi  23141  ovolunlem1  23311  ulmclm  24186  ulmcaulem  24193  ulmcau  24194  ulmss  24196  rlimcnp  24737  cxploglim  24749  lgsdchr  25125  pntlemp  25344  axcontlem4  25892  ewlkle  26557  uspgr2wlkeq  26598  umgrwlknloop  26601  wlkiswwlksupgr2  26831  3cyclfrgrrn2  27267  nmlnoubi  27779  lnon0  27781  disjpreima  29523  resspos  29787  resstos  29788  submarchi  29868  crefss  30044  iccllysconn  31358  cvmlift2lem1  31410  ss2mcls  31591  mclsax  31592  nosupno  31974  nosupres  31978  sssslt2  32032  poimirlem25  33564  poimirlem27  33566  upixp  33654  caushft  33687  sstotbnd3  33705  totbndss  33706  unichnidl  33960  ispridl2  33967  elrfirn2  37576  mzpsubst  37628  eluzrabdioph  37687  neik0pk1imk0  38662  limsupub  40254  limsupre3lem  40282  climuzlem  40293  xlimbr  40371  fourierdlem103  40744  fourierdlem104  40745  qndenserrnbllem  40832  ralralimp  41619