Theorem ralimdv 2963

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  poss  5037  sess1  5082  sess2  5083  riinint  5382  iinpreima  6345  dffo4  6375  dffo5  6376  isoini2  6589  tfindsg  7060  el2mpt2csbcl  7250  iiner  7819  xpf1o  8122  dffi3  8337  brwdom3  8487  xpwdomg  8490  bndrank  8704  cfub  9071  cff1  9080  cfflb  9081  cfslb2n  9090  cofsmo  9091  cfcoflem  9094  pwcfsdom  9405  fpwwe2lem13  9464  inawinalem  9511  grupr  9619  fsequb  12774  cau3lem  14094  caubnd2  14097  caubnd  14098  rlim2lt  14228  rlim3  14229  climshftlem  14305  isercolllem1  14395  climcau  14401  caucvgb  14410  serf0  14411  modfsummods  14525  cvgcmp  14548  mreriincl  16258  acsfn1c  16323  islss4  18962  riinopn  20713  fiinbas  20756  baspartn  20758  isclo2  20892  lmcls  21106  lmcnp  21108  isnrm3  21163  1stcelcls  21264  llyss  21282  nllyss  21283  ptpjpre1  21374  txlly  21439  txnlly  21440  tx1stc  21453  xkococnlem  21462  fbunfip  21673  filssufilg  21715  cnpflf2  21804  fcfnei  21839  isucn2  22083  rescncf  22700  lebnum  22763  cfilss  23068  fgcfil  23069  iscau4  23077  cmetcaulem  23086  cfilres  23094  caussi  23095  ovolunlem1  23265  ulmclm  24141  ulmcaulem  24148  ulmcau  24149  ulmss  24151  rlimcnp  24692  cxploglim  24704  lgsdchr  25080  pntlemp  25299  axcontlem4  25847  ewlkle  26501  uspgr2wlkeq  26542  umgrwlknloop  26545  wlkiswwlksupgr2  26763  3cyclfrgrrn2  27151  nmlnoubi  27651  lnon0  27653  disjpreima  29397  resspos  29659  resstos  29660  submarchi  29740  crefss  29916  iccllysconn  31232  cvmlift2lem1  31284  ss2mcls  31465  mclsax  31466  nosupno  31849  nosupres  31853  sssslt2  31907  poimirlem25  33434  poimirlem27  33436  upixp  33524  caushft  33557  sstotbnd3  33575  totbndss  33576  unichnidl  33830  ispridl2  33837  elrfirn2  37259  mzpsubst  37311  eluzrabdioph  37370  neik0pk1imk0  38345  limsupub  39936  limsupre3lem  39964  climuzlem  39975  xlimbr  40053  fourierdlem103  40426  fourierdlem104  40427  qndenserrnbllem  40514  ralralimp  41295