Theorem ralimdv 3169

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 3167	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3061

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 3062

This theorem is referenced by:  r19.21v  3180  ss2ralv  4054  poss  5594  sess1  5650  sess2  5651  riinint  5982  iinpreima  7089  dffo4  7123  dffo5  7124  isoini2  7359  tfindsg  7882  el2mpocsbcl  8110  xpord3inddlem  8179  iiner  8829  xpf1o  9179  dffi3  9471  brwdom3  9622  xpwdomg  9625  ttrclss  9760  bndrank  9881  cfub  10289  cff1  10298  cfflb  10299  cfslb2n  10308  cofsmo  10309  cfcoflem  10312  pwcfsdom  10623  fpwwe2lem12  10682  inawinalem  10729  grupr  10837  fsequb  14016  cau3lem  15393  caubnd2  15396  caubnd  15397  rlim2lt  15533  rlim3  15534  climshftlem  15610  climcau  15707  caucvgb  15716  serf0  15717  modfsummods  15829  cvgcmp  15852  mreriincl  17641  acsfn1c  17705  islss4  20960  riinopn  22914  fiinbas  22959  baspartn  22961  isclo2  23096  lmcls  23310  lmcnp  23312  isnrm3  23367  1stcelcls  23469  llyss  23487  nllyss  23488  ptpjpre1  23579  txlly  23644  txnlly  23645  tx1stc  23658  xkococnlem  23667  fbunfip  23877  filssufilg  23919  cnpflf2  24008  fcfnei  24043  isucn2  24288  rescncf  24923  lebnum  24996  cfilss  25304  fgcfil  25305  iscau4  25313  cmetcaulem  25322  caussi  25331  ovolunlem1  25532  ulmclm  26430  ulmcaulem  26437  ulmcau  26438  ulmss  26440  rlimcnp  27008  cxploglim  27021  2sqreunnlem2  27499  pntlemp  27654  nosupno  27748  nosupres  27752  noinfno  27763  noinfres  27767  sssslt2  27841  madebdayim  27926  madebdaylemold  27936  axcontlem4  28982  ewlkle  29623  uspgr2wlkeq  29664  umgrwlknloop  29667  wlkiswwlksupgr2  29897  3cyclfrgrrn2  30306  nmlnoubi  30815  lnon0  30817  disjpreima  32597  resspos  32956  resstos  32957  submarchi  33193  prmidl2  33469  crefss  33848  iccllysconn  35255  cvmlift2lem1  35307  dmopab3rexdif  35410  ss2mcls  35573  mclsax  35574  isinf2  37406  poimirlem25  37652  poimirlem27  37654  upixp  37736  caushft  37768  sstotbnd3  37783  totbndss  37784  unichnidl  38038  ispridl2  38045  elrfirn2  42707  mzpsubst  42759  eluzrabdioph  42817  neik0pk1imk0  44060  mnuop3d  44290  ismnushort  44320  pwclaxpow  45001  limsupub  45719  limsupre3lem  45747  climuzlem  45758  xlimbr  45842  fourierdlem103  46224  fourierdlem104  46225  qndenserrnbllem  46309  2reuimp  47127  ralralimp  47290