Theorem ralimdv 3185

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  r19.21v  3196  ralimdvv  3220  ss2ralv  4016  poss  5572  sess1  5627  sess2  5628  riinint  5963  iinpreima  7065  dffo4  7099  dffo5  7100  isoini2  7338  tfindsg  7857  el2mpocsbcl  8080  xpord3inddlem  8150  iiner  8787  xpf1o  9127  dffi3  9391  brwdom3  9544  xpwdomg  9547  ttrclss  9689  bndrank  9813  cfub  10232  cff1  10242  cfflb  10243  cfslb2n  10252  cofsmo  10253  cfcoflem  10256  pwcfsdom  10568  fpwwe2lem12  10627  inawinalem  10674  grupr  10782  fsequb  14011  cau3lem  15406  caubnd2  15409  caubnd  15410  rlim2lt  15548  rlim3  15549  climshftlem  15625  climcau  15722  caucvgb  15731  serf0  15732  modfsummods  15845  cvgcmp  15868  mreriincl  17650  acsfn1c  17718  resspos  18485  resstos  18486  chnrss  18671  islss4  21061  unichnlidl  21340  prmidl2  21437  riinopn  23034  fiinbas  23078  baspartn  23080  isclo2  23214  lmcls  23428  lmcnp  23430  isnrm3  23485  1stcelcls  23587  llyss  23605  nllyss  23606  ptpjpre1  23697  txlly  23762  txnlly  23763  tx1stc  23776  xkococnlem  23785  fbunfip  23995  filssufilg  24037  cnpflf2  24126  fcfnei  24161  isucn2  24404  rescncf  25025  lebnum  25092  cfilss  25398  fgcfil  25399  iscau4  25407  cmetcaulem  25416  caussi  25425  ovolunlem1  25625  ulmclm  26516  ulmcaulem  26523  ulmcau  26524  ulmss  26526  rlimcnp  27096  cxploglim  27108  2sqreunnlem2  27585  pntlemp  27740  nosupno  27833  nosupres  27837  noinfno  27848  noinfres  27852  ssslts2  27933  madebdayim  28047  madebdaylemold  28057  axcontlem4  29258  ewlkle  29896  uspgr2wlkeq  29936  umgrwlknloop  29939  wlkiswwlksupgr2  30167  3cyclfrgrrn2  30579  nmlnoubi  31089  lnon0  31091  disjpreima  32870  submarchi  33447  crefss  34184  r1filimi  35440  iccllysconn  35675  cvmlift2lem1  35727  dmopab3rexdif  35830  ss2mcls  35993  mclsax  35994  dfttc4lem2  36963  isinf2  37973  poimirlem25  38218  poimirlem27  38220  upixp  38302  caushft  38334  sstotbnd3  38349  totbndss  38350  unichnidl  38604  ispridl2  38611  elrfirn2  43353  mzpsubst  43405  eluzrabdioph  43459  neik0pk1imk0  44699  mnuop3d  44907  ismnushort  44937  pwclaxpow  45619  limsupub  46344  limsupre3lem  46372  climuzlem  46383  xlimbr  46467  fourierdlem103  46849  fourierdlem104  46850  qndenserrnbllem  46934  2reuimp  47775  ralralimp  47938