Theorem ralimdv 3143

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 3141	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  3154  ralimdvv  3178  ss2ralv  4006  poss  5529  sess1  5584  sess2  5585  riinint  5913  iinpreima  7003  dffo4  7037  dffo5  7038  isoini2  7276  tfindsg  7794  el2mpocsbcl  8018  xpord3inddlem  8087  iiner  8716  xpf1o  9056  dffi3  9321  brwdom3  9474  xpwdomg  9477  ttrclss  9616  bndrank  9737  cfub  10143  cff1  10152  cfflb  10153  cfslb2n  10162  cofsmo  10163  cfcoflem  10166  pwcfsdom  10477  fpwwe2lem12  10536  inawinalem  10583  grupr  10691  fsequb  13882  cau3lem  15262  caubnd2  15265  caubnd  15266  rlim2lt  15404  rlim3  15405  climshftlem  15481  climcau  15578  caucvgb  15587  serf0  15588  modfsummods  15700  cvgcmp  15723  mreriincl  17500  acsfn1c  17568  resspos  18335  resstos  18336  islss4  20865  riinopn  22793  fiinbas  22837  baspartn  22839  isclo2  22973  lmcls  23187  lmcnp  23189  isnrm3  23244  1stcelcls  23346  llyss  23364  nllyss  23365  ptpjpre1  23456  txlly  23521  txnlly  23522  tx1stc  23535  xkococnlem  23544  fbunfip  23754  filssufilg  23796  cnpflf2  23885  fcfnei  23920  isucn2  24164  rescncf  24788  lebnum  24861  cfilss  25168  fgcfil  25169  iscau4  25177  cmetcaulem  25186  caussi  25195  ovolunlem1  25396  ulmclm  26294  ulmcaulem  26301  ulmcau  26302  ulmss  26304  rlimcnp  26873  cxploglim  26886  2sqreunnlem2  27364  pntlemp  27519  nosupno  27613  nosupres  27617  noinfno  27628  noinfres  27632  sssslt2  27707  madebdayim  27802  madebdaylemold  27812  axcontlem4  28912  ewlkle  29551  uspgr2wlkeq  29591  umgrwlknloop  29594  wlkiswwlksupgr2  29822  3cyclfrgrrn2  30231  nmlnoubi  30740  lnon0  30742  disjpreima  32528  submarchi  33129  prmidl2  33379  crefss  33822  iccllysconn  35233  cvmlift2lem1  35285  dmopab3rexdif  35388  ss2mcls  35551  mclsax  35552  isinf2  37389  poimirlem25  37635  poimirlem27  37637  upixp  37719  caushft  37751  sstotbnd3  37766  totbndss  37767  unichnidl  38021  ispridl2  38028  elrfirn2  42679  mzpsubst  42731  eluzrabdioph  42789  neik0pk1imk0  44030  mnuop3d  44254  ismnushort  44284  pwclaxpow  44968  limsupub  45695  limsupre3lem  45723  climuzlem  45734  xlimbr  45818  fourierdlem103  46200  fourierdlem104  46201  qndenserrnbllem  46285  2reuimp  47109  ralralimp  47272