Theorem ralimdv 3145

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  ss2ralv  3983  poss  5440  sess1  5487  sess2  5488  riinint  5804  iinpreima  6814  dffo4  6846  dffo5  6847  isoini2  7071  tfindsg  7555  el2mpocsbcl  7763  iiner  8352  xpf1o  8663  dffi3  8879  brwdom3  9030  xpwdomg  9033  bndrank  9254  cfub  9660  cff1  9669  cfflb  9670  cfslb2n  9679  cofsmo  9680  cfcoflem  9683  pwcfsdom  9994  fpwwe2lem13  10053  inawinalem  10100  grupr  10208  fsequb  13338  cau3lem  14706  caubnd2  14709  caubnd  14710  rlim2lt  14846  rlim3  14847  climshftlem  14923  climcau  15019  caucvgb  15028  serf0  15029  modfsummods  15140  cvgcmp  15163  mreriincl  16861  acsfn1c  16925  islss4  19727  riinopn  21513  fiinbas  21557  baspartn  21559  isclo2  21693  lmcls  21907  lmcnp  21909  isnrm3  21964  1stcelcls  22066  llyss  22084  nllyss  22085  ptpjpre1  22176  txlly  22241  txnlly  22242  tx1stc  22255  xkococnlem  22264  fbunfip  22474  filssufilg  22516  cnpflf2  22605  fcfnei  22640  isucn2  22885  rescncf  23502  lebnum  23569  cfilss  23874  fgcfil  23875  iscau4  23883  cmetcaulem  23892  caussi  23901  ovolunlem1  24101  ulmclm  24982  ulmcaulem  24989  ulmcau  24990  ulmss  24992  rlimcnp  25551  cxploglim  25563  2sqreunnlem2  26039  pntlemp  26194  axcontlem4  26761  ewlkle  27395  uspgr2wlkeq  27435  umgrwlknloop  27438  wlkiswwlksupgr2  27663  3cyclfrgrrn2  28072  nmlnoubi  28579  lnon0  28581  disjpreima  30347  resspos  30672  resstos  30673  submarchi  30865  prmidl2  31024  crefss  31202  iccllysconn  32610  cvmlift2lem1  32662  dmopab3rexdif  32765  ss2mcls  32928  mclsax  32929  nosupno  33316  nosupres  33320  sssslt2  33374  isinf2  34822  poimirlem25  35082  poimirlem27  35084  upixp  35167  caushft  35199  sstotbnd3  35214  totbndss  35215  unichnidl  35469  ispridl2  35476  elrfirn2  39637  mzpsubst  39689  eluzrabdioph  39747  neik0pk1imk0  40750  mnuop3d  40979  limsupub  42346  limsupre3lem  42374  climuzlem  42385  xlimbr  42469  fourierdlem103  42851  fourierdlem104  42852  qndenserrnbllem  42936  2reuimp  43671  ralralimp  43834