Theorem ralimdv 3103

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  ss2ralv  3985  poss  5496  sess1  5548  sess2  5549  riinint  5866  iinpreima  6928  dffo4  6961  dffo5  6962  isoini2  7190  tfindsg  7682  el2mpocsbcl  7896  iiner  8536  xpf1o  8875  dffi3  9120  brwdom3  9271  xpwdomg  9274  bndrank  9530  cfub  9936  cff1  9945  cfflb  9946  cfslb2n  9955  cofsmo  9956  cfcoflem  9959  pwcfsdom  10270  fpwwe2lem12  10329  inawinalem  10376  grupr  10484  fsequb  13623  cau3lem  14994  caubnd2  14997  caubnd  14998  rlim2lt  15134  rlim3  15135  climshftlem  15211  climcau  15310  caucvgb  15319  serf0  15320  modfsummods  15433  cvgcmp  15456  mreriincl  17224  acsfn1c  17288  islss4  20139  riinopn  21965  fiinbas  22010  baspartn  22012  isclo2  22147  lmcls  22361  lmcnp  22363  isnrm3  22418  1stcelcls  22520  llyss  22538  nllyss  22539  ptpjpre1  22630  txlly  22695  txnlly  22696  tx1stc  22709  xkococnlem  22718  fbunfip  22928  filssufilg  22970  cnpflf2  23059  fcfnei  23094  isucn2  23339  rescncf  23966  lebnum  24033  cfilss  24339  fgcfil  24340  iscau4  24348  cmetcaulem  24357  caussi  24366  ovolunlem1  24566  ulmclm  25451  ulmcaulem  25458  ulmcau  25459  ulmss  25461  rlimcnp  26020  cxploglim  26032  2sqreunnlem2  26508  pntlemp  26663  axcontlem4  27238  ewlkle  27875  uspgr2wlkeq  27915  umgrwlknloop  27918  wlkiswwlksupgr2  28143  3cyclfrgrrn2  28552  nmlnoubi  29059  lnon0  29061  disjpreima  30824  resspos  31146  resstos  31147  submarchi  31342  prmidl2  31518  crefss  31701  iccllysconn  33112  cvmlift2lem1  33164  dmopab3rexdif  33267  ss2mcls  33430  mclsax  33431  ttrclss  33706  nosupno  33833  nosupres  33837  noinfno  33848  noinfres  33852  sssslt2  33917  madebdayim  33997  madebdaylemold  34005  isinf2  35503  poimirlem25  35729  poimirlem27  35731  upixp  35814  caushft  35846  sstotbnd3  35861  totbndss  35862  unichnidl  36116  ispridl2  36123  elrfirn2  40434  mzpsubst  40486  eluzrabdioph  40544  neik0pk1imk0  41546  mnuop3d  41778  ismnushort  41808  limsupub  43135  limsupre3lem  43163  climuzlem  43174  xlimbr  43258  fourierdlem103  43640  fourierdlem104  43641  qndenserrnbllem  43725  2reuimp  44494  ralralimp  44657