Theorem ralimdv 3109

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3069

This theorem is referenced by:  r19.21v  3113  ss2ralv  3989  poss  5505  sess1  5557  sess2  5558  riinint  5877  iinpreima  6946  dffo4  6979  dffo5  6980  isoini2  7210  tfindsg  7707  el2mpocsbcl  7925  iiner  8578  xpf1o  8926  dffi3  9190  brwdom3  9341  xpwdomg  9344  ttrclss  9478  bndrank  9599  cfub  10005  cff1  10014  cfflb  10015  cfslb2n  10024  cofsmo  10025  cfcoflem  10028  pwcfsdom  10339  fpwwe2lem12  10398  inawinalem  10445  grupr  10553  fsequb  13695  cau3lem  15066  caubnd2  15069  caubnd  15070  rlim2lt  15206  rlim3  15207  climshftlem  15283  climcau  15382  caucvgb  15391  serf0  15392  modfsummods  15505  cvgcmp  15528  mreriincl  17307  acsfn1c  17371  islss4  20224  riinopn  22057  fiinbas  22102  baspartn  22104  isclo2  22239  lmcls  22453  lmcnp  22455  isnrm3  22510  1stcelcls  22612  llyss  22630  nllyss  22631  ptpjpre1  22722  txlly  22787  txnlly  22788  tx1stc  22801  xkococnlem  22810  fbunfip  23020  filssufilg  23062  cnpflf2  23151  fcfnei  23186  isucn2  23431  rescncf  24060  lebnum  24127  cfilss  24434  fgcfil  24435  iscau4  24443  cmetcaulem  24452  caussi  24461  ovolunlem1  24661  ulmclm  25546  ulmcaulem  25553  ulmcau  25554  ulmss  25556  rlimcnp  26115  cxploglim  26127  2sqreunnlem2  26603  pntlemp  26758  axcontlem4  27335  ewlkle  27972  uspgr2wlkeq  28013  umgrwlknloop  28016  wlkiswwlksupgr2  28242  3cyclfrgrrn2  28651  nmlnoubi  29158  lnon0  29160  disjpreima  30923  resspos  31244  resstos  31245  submarchi  31440  prmidl2  31616  crefss  31799  iccllysconn  33212  cvmlift2lem1  33264  dmopab3rexdif  33367  ss2mcls  33530  mclsax  33531  nosupno  33906  nosupres  33910  noinfno  33921  noinfres  33925  sssslt2  33990  madebdayim  34070  madebdaylemold  34078  isinf2  35576  poimirlem25  35802  poimirlem27  35804  upixp  35887  caushft  35919  sstotbnd3  35934  totbndss  35935  unichnidl  36189  ispridl2  36196  elrfirn2  40518  mzpsubst  40570  eluzrabdioph  40628  neik0pk1imk0  41657  mnuop3d  41889  ismnushort  41919  limsupub  43245  limsupre3lem  43273  climuzlem  43284  xlimbr  43368  fourierdlem103  43750  fourierdlem104  43751  qndenserrnbllem  43835  2reuimp  44607  ralralimp  44770