Theorem ralimdv 3176

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

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

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 3077

This theorem is used by:  r19.21v  3187  ralimdvv  3211  ss2ralv  4002  poss  5565  sess1  5620  sess2  5621  riinint  5956  iinpreima  7063  dffo4  7097  dffo5  7098  isoini2  7341  tfindsg  7858  el2mpocsbcl  8083  xpord3inddlem  8153  iiner  8792  xpf1o  9140  dffi3  9404  brwdom3  9557  xpwdomg  9560  ttrclss  9702  bndrank  9826  cfub  10253  cff1  10263  cfflb  10264  cfslb2n  10273  cofsmo  10274  cfcoflem  10277  pwcfsdom  10595  fpwwe2lem12  10654  inawinalem  10701  grupr  10809  fsequb  14042  cau3lem  15445  caubnd2  15448  caubnd  15449  rlim2lt  15587  rlim3  15588  climshftlem  15664  climcau  15761  caucvgb  15770  serf0  15771  modfsummods  15883  cvgcmp  15906  mreriincl  17685  acsfn1c  17753  resspos  18520  resstos  18521  chnrss  18706  islss4  21149  unichnlidl  21428  prmidl2  21532  riinopn  23136  fiinbas  23180  baspartn  23182  isclo2  23316  lmcls  23530  lmcnp  23532  isnrm3  23587  1stcelcls  23690  llyss  23708  nllyss  23709  ptpjpre1  23800  txlly  23865  txnlly  23866  tx1stc  23879  xkococnlem  23888  fbunfip  24098  filssufilg  24140  cnpflf2  24229  fcfnei  24264  isucn2  24507  rescncf  25128  lebnum  25195  cfilss  25501  fgcfil  25502  iscau4  25510  cmetcaulem  25519  caussi  25528  ovolunlem1  25728  ulmclm  26626  ulmcaulem  26633  ulmcau  26634  ulmss  26636  rlimcnp  27205  cxploglim  27217  2sqreunnlem2  27694  pntlemp  27849  nosupno  27942  nosupres  27946  noinfno  27957  noinfres  27961  ssslts2  28042  madebdayim  28156  madebdaylemold  28166  axcontlem4  29427  ewlkle  30068  uspgr2wlkeq  30108  umgrwlknloop  30111  wlkiswwlksupgr2  30348  3cyclfrgrrn2  30770  nmlnoubi  31280  lnon0  31282  disjpreima  33060  submarchi  33629  crefss  34362  r1filimi  35614  iccllysconn  35832  cvmlift2lem1  35884  dmopab3rexdif  35987  ss2mcls  36150  mclsax  36151  dfttc4lem2  37151  isinf2  38162  poimirlem25  38397  poimirlem27  38399  upixp  38482  caushft  38514  sstotbnd3  38529  totbndss  38530  unichnidl  38784  ispridl2  38791  elrfirn2  43544  mzpsubst  43596  eluzrabdioph  43650  neik0pk1imk0  44890  mnuop3d  45098  ismnushort  45128  pwclaxpow  45810  limsupub  46535  limsupre3lem  46563  climuzlem  46574  xlimbr  46658  fourierdlem103  47040  fourierdlem104  47041  qndenserrnbllem  47125  2reuimp  48006  ralralimp  48169