Theorem ralimdv 3166

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  r19.21v  3177  ss2ralv  4065  poss  5598  sess1  5653  sess2  5654  riinint  5984  iinpreima  7088  dffo4  7122  dffo5  7123  isoini2  7358  tfindsg  7881  el2mpocsbcl  8108  xpord3inddlem  8177  iiner  8827  xpf1o  9177  dffi3  9468  brwdom3  9619  xpwdomg  9622  ttrclss  9757  bndrank  9878  cfub  10286  cff1  10295  cfflb  10296  cfslb2n  10305  cofsmo  10306  cfcoflem  10309  pwcfsdom  10620  fpwwe2lem12  10679  inawinalem  10726  grupr  10834  fsequb  14012  cau3lem  15389  caubnd2  15392  caubnd  15393  rlim2lt  15529  rlim3  15530  climshftlem  15606  climcau  15703  caucvgb  15712  serf0  15713  modfsummods  15825  cvgcmp  15848  mreriincl  17642  acsfn1c  17706  islss4  20977  riinopn  22929  fiinbas  22974  baspartn  22976  isclo2  23111  lmcls  23325  lmcnp  23327  isnrm3  23382  1stcelcls  23484  llyss  23502  nllyss  23503  ptpjpre1  23594  txlly  23659  txnlly  23660  tx1stc  23673  xkococnlem  23682  fbunfip  23892  filssufilg  23934  cnpflf2  24023  fcfnei  24058  isucn2  24303  rescncf  24936  lebnum  25009  cfilss  25317  fgcfil  25318  iscau4  25326  cmetcaulem  25335  caussi  25344  ovolunlem1  25545  ulmclm  26444  ulmcaulem  26451  ulmcau  26452  ulmss  26454  rlimcnp  27022  cxploglim  27035  2sqreunnlem2  27513  pntlemp  27668  nosupno  27762  nosupres  27766  noinfno  27777  noinfres  27781  sssslt2  27855  madebdayim  27940  madebdaylemold  27950  axcontlem4  28996  ewlkle  29637  uspgr2wlkeq  29678  umgrwlknloop  29681  wlkiswwlksupgr2  29906  3cyclfrgrrn2  30315  nmlnoubi  30824  lnon0  30826  disjpreima  32603  resspos  32940  resstos  32941  submarchi  33175  prmidl2  33448  crefss  33809  iccllysconn  35234  cvmlift2lem1  35286  dmopab3rexdif  35389  ss2mcls  35552  mclsax  35553  isinf2  37387  poimirlem25  37631  poimirlem27  37633  upixp  37715  caushft  37747  sstotbnd3  37762  totbndss  37763  unichnidl  38017  ispridl2  38024  elrfirn2  42683  mzpsubst  42735  eluzrabdioph  42793  neik0pk1imk0  44036  mnuop3d  44266  ismnushort  44296  limsupub  45659  limsupre3lem  45687  climuzlem  45698  xlimbr  45782  fourierdlem103  46164  fourierdlem104  46165  qndenserrnbllem  46249  2reuimp  47064  ralralimp  47227