Theorem ralimdv 3147

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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 3045

This theorem is referenced by:  r19.21v  3158  ralimdvv  3184  ss2ralv  4014  poss  5541  sess1  5596  sess2  5597  riinint  5924  iinpreima  7023  dffo4  7057  dffo5  7058  isoini2  7296  tfindsg  7817  el2mpocsbcl  8041  xpord3inddlem  8110  iiner  8739  xpf1o  9080  dffi3  9358  brwdom3  9511  xpwdomg  9514  ttrclss  9649  bndrank  9770  cfub  10178  cff1  10187  cfflb  10188  cfslb2n  10197  cofsmo  10198  cfcoflem  10201  pwcfsdom  10512  fpwwe2lem12  10571  inawinalem  10618  grupr  10726  fsequb  13916  cau3lem  15297  caubnd2  15300  caubnd  15301  rlim2lt  15439  rlim3  15440  climshftlem  15516  climcau  15613  caucvgb  15622  serf0  15623  modfsummods  15735  cvgcmp  15758  mreriincl  17535  acsfn1c  17603  resspos  18370  resstos  18371  islss4  20900  riinopn  22828  fiinbas  22872  baspartn  22874  isclo2  23008  lmcls  23222  lmcnp  23224  isnrm3  23279  1stcelcls  23381  llyss  23399  nllyss  23400  ptpjpre1  23491  txlly  23556  txnlly  23557  tx1stc  23570  xkococnlem  23579  fbunfip  23789  filssufilg  23831  cnpflf2  23920  fcfnei  23955  isucn2  24199  rescncf  24823  lebnum  24896  cfilss  25203  fgcfil  25204  iscau4  25212  cmetcaulem  25221  caussi  25230  ovolunlem1  25431  ulmclm  26329  ulmcaulem  26336  ulmcau  26337  ulmss  26339  rlimcnp  26908  cxploglim  26921  2sqreunnlem2  27399  pntlemp  27554  nosupno  27648  nosupres  27652  noinfno  27663  noinfres  27667  sssslt2  27742  madebdayim  27837  madebdaylemold  27847  axcontlem4  28947  ewlkle  29586  uspgr2wlkeq  29626  umgrwlknloop  29629  wlkiswwlksupgr2  29857  3cyclfrgrrn2  30266  nmlnoubi  30775  lnon0  30777  disjpreima  32563  submarchi  33155  prmidl2  33405  crefss  33832  iccllysconn  35230  cvmlift2lem1  35282  dmopab3rexdif  35385  ss2mcls  35548  mclsax  35549  isinf2  37386  poimirlem25  37632  poimirlem27  37634  upixp  37716  caushft  37748  sstotbnd3  37763  totbndss  37764  unichnidl  38018  ispridl2  38025  elrfirn2  42677  mzpsubst  42729  eluzrabdioph  42787  neik0pk1imk0  44029  mnuop3d  44253  ismnushort  44283  pwclaxpow  44967  limsupub  45695  limsupre3lem  45723  climuzlem  45734  xlimbr  45818  fourierdlem103  46200  fourierdlem104  46201  qndenserrnbllem  46285  2reuimp  47109  ralralimp  47272