Theorem ralimdv 3177

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3078

This theorem is used by:  r19.21v  3188  ralimdvv  3212  ss2ralv  4002  poss  5561  sess1  5616  sess2  5617  riinint  5954  iinpreima  7069  dffo4  7103  dffo5  7104  isoini2  7347  tfindsg  7872  el2mpocsbcl  8096  xpord3inddlem  8171  iiner  8810  xpf1o  9158  dffi3  9423  brwdom3  9576  xpwdomg  9579  ttrclss  9721  bndrank  9854  r1filimi  9903  cfub  10326  cff1  10336  cfflb  10337  cfslb2n  10346  cofsmo  10347  cfcoflem  10350  pwcfsdom  10668  fpwwe2lem12  10727  inawinalem  10774  grupr  10882  fsequb  14118  cau3lem  15522  caubnd2  15525  caubnd  15526  rlim2lt  15664  rlim3  15665  climshftlem  15741  climcau  15838  caucvgb  15847  serf0  15848  modfsummods  15960  cvgcmp  15983  mreriincl  17768  acsfn1c  17836  resspos  18603  resstos  18604  chnrss  18789  islss4  21237  unichnlidl  21516  prmidl2  21622  riinopn  23226  fiinbas  23270  baspartn  23272  isclo2  23406  lmcls  23620  lmcnp  23622  isnrm3  23677  1stcelcls  23780  llyss  23798  nllyss  23799  ptpjpre1  23890  txlly  23955  txnlly  23956  tx1stc  23969  xkococnlem  23978  fbunfip  24188  filssufilg  24230  cnpflf2  24319  fcfnei  24354  isucn2  24597  rescncf  25218  lebnum  25285  cfilss  25591  fgcfil  25592  iscau4  25600  cmetcaulem  25609  caussi  25618  ovolunlem1  25818  ulmclm  26714  ulmcaulem  26721  ulmcau  26722  ulmss  26724  rlimcnp  27293  cxploglim  27305  2sqreunnlem2  27782  pntlemp  27937  nosupno  28060  nosupres  28064  noinfno  28075  noinfres  28079  ssslts2  28160  madebdayim  28274  madebdaylemold  28284  axcontlem4  29545  ewlkle  30186  uspgr2wlkeq  30226  umgrwlknloop  30229  wlkiswwlksupgr2  30466  3cyclfrgrrn2  30888  nmlnoubi  31398  lnon0  31400  disjpreima  33178  submarchi  33747  crefss  34481  iccllysconn  36015  cvmlift2lem1  36067  dmopab3rexdif  36170  ss2mcls  36333  mclsax  36334  dfttc4lem2  37317  isinf2  38328  poimirlem25  38563  poimirlem27  38565  upixp  38663  caushft  38695  sstotbnd3  38710  totbndss  38711  unichnidl  38965  ispridl2  38972  elrfirn2  43706  mzpsubst  43758  eluzrabdioph  43812  neik0pk1imk0  45046  mnuop3d  45254  ismnushort  45284  pwclaxpow  45973  limsupub  46713  limsupre3lem  46741  climuzlem  46752  xlimbr  46836  fourierdlem103  47218  fourierdlem104  47219  qndenserrnbllem  47303  2reuimp  48184  ralralimp  48347