Theorem ralimdv 3167

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 479	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3165	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  r19.21v  3177  ss2ralv  4051  poss  5589  sess1  5643  sess2  5644  riinint  5966  iinpreima  7069  dffo4  7103  dffo5  7104  isoini2  7338  tfindsg  7852  el2mpocsbcl  8073  xpord3inddlem  8142  iiner  8785  xpf1o  9141  dffi3  9428  brwdom3  9579  xpwdomg  9582  ttrclss  9717  bndrank  9838  cfub  10246  cff1  10255  cfflb  10256  cfslb2n  10265  cofsmo  10266  cfcoflem  10269  pwcfsdom  10580  fpwwe2lem12  10639  inawinalem  10686  grupr  10794  fsequb  13944  cau3lem  15305  caubnd2  15308  caubnd  15309  rlim2lt  15445  rlim3  15446  climshftlem  15522  climcau  15621  caucvgb  15630  serf0  15631  modfsummods  15743  cvgcmp  15766  mreriincl  17546  acsfn1c  17610  islss4  20717  riinopn  22630  fiinbas  22675  baspartn  22677  isclo2  22812  lmcls  23026  lmcnp  23028  isnrm3  23083  1stcelcls  23185  llyss  23203  nllyss  23204  ptpjpre1  23295  txlly  23360  txnlly  23361  tx1stc  23374  xkococnlem  23383  fbunfip  23593  filssufilg  23635  cnpflf2  23724  fcfnei  23759  isucn2  24004  rescncf  24637  lebnum  24710  cfilss  25018  fgcfil  25019  iscau4  25027  cmetcaulem  25036  caussi  25045  ovolunlem1  25246  ulmclm  26135  ulmcaulem  26142  ulmcau  26143  ulmss  26145  rlimcnp  26706  cxploglim  26718  2sqreunnlem2  27194  pntlemp  27349  nosupno  27442  nosupres  27446  noinfno  27457  noinfres  27461  sssslt2  27534  madebdayim  27619  madebdaylemold  27629  axcontlem4  28492  ewlkle  29129  uspgr2wlkeq  29170  umgrwlknloop  29173  wlkiswwlksupgr2  29398  3cyclfrgrrn2  29807  nmlnoubi  30316  lnon0  30318  disjpreima  32082  resspos  32403  resstos  32404  submarchi  32602  prmidl2  32833  crefss  33127  iccllysconn  34539  cvmlift2lem1  34591  dmopab3rexdif  34694  ss2mcls  34857  mclsax  34858  isinf2  36589  poimirlem25  36816  poimirlem27  36818  upixp  36900  caushft  36932  sstotbnd3  36947  totbndss  36948  unichnidl  37202  ispridl2  37209  elrfirn2  41736  mzpsubst  41788  eluzrabdioph  41846  neik0pk1imk0  43100  mnuop3d  43332  ismnushort  43362  limsupub  44718  limsupre3lem  44746  climuzlem  44757  xlimbr  44841  fourierdlem103  45223  fourierdlem104  45224  qndenserrnbllem  45308  2reuimp  46121  ralralimp  46284