Theorem ralimdv 3150

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3051

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  r19.21v  3161  ralimdvv  3185  ss2ralv  4004  poss  5534  sess1  5589  sess2  5590  riinint  5921  iinpreima  7014  dffo4  7048  dffo5  7049  isoini2  7285  tfindsg  7803  el2mpocsbcl  8027  xpord3inddlem  8096  iiner  8726  xpf1o  9067  dffi3  9334  brwdom3  9487  xpwdomg  9490  ttrclss  9629  bndrank  9753  cfub  10159  cff1  10168  cfflb  10169  cfslb2n  10178  cofsmo  10179  cfcoflem  10182  pwcfsdom  10494  fpwwe2lem12  10553  inawinalem  10600  grupr  10708  fsequb  13898  cau3lem  15278  caubnd2  15281  caubnd  15282  rlim2lt  15420  rlim3  15421  climshftlem  15497  climcau  15594  caucvgb  15603  serf0  15604  modfsummods  15716  cvgcmp  15739  mreriincl  17517  acsfn1c  17585  resspos  18352  resstos  18353  chnrss  18538  islss4  20913  riinopn  22852  fiinbas  22896  baspartn  22898  isclo2  23032  lmcls  23246  lmcnp  23248  isnrm3  23303  1stcelcls  23405  llyss  23423  nllyss  23424  ptpjpre1  23515  txlly  23580  txnlly  23581  tx1stc  23594  xkococnlem  23603  fbunfip  23813  filssufilg  23855  cnpflf2  23944  fcfnei  23979  isucn2  24222  rescncf  24846  lebnum  24919  cfilss  25226  fgcfil  25227  iscau4  25235  cmetcaulem  25244  caussi  25253  ovolunlem1  25454  ulmclm  26352  ulmcaulem  26359  ulmcau  26360  ulmss  26362  rlimcnp  26931  cxploglim  26944  2sqreunnlem2  27422  pntlemp  27577  nosupno  27671  nosupres  27675  noinfno  27686  noinfres  27690  ssslts2  27770  madebdayim  27884  madebdaylemold  27894  axcontlem4  29040  ewlkle  29679  uspgr2wlkeq  29719  umgrwlknloop  29722  wlkiswwlksupgr2  29950  3cyclfrgrrn2  30362  nmlnoubi  30871  lnon0  30873  disjpreima  32659  submarchi  33268  prmidl2  33522  crefss  34006  r1filimi  35259  iccllysconn  35444  cvmlift2lem1  35496  dmopab3rexdif  35599  ss2mcls  35762  mclsax  35763  isinf2  37610  poimirlem25  37846  poimirlem27  37848  upixp  37930  caushft  37962  sstotbnd3  37977  totbndss  37978  unichnidl  38232  ispridl2  38239  elrfirn2  42948  mzpsubst  43000  eluzrabdioph  43058  neik0pk1imk0  44298  mnuop3d  44522  ismnushort  44552  pwclaxpow  45235  limsupub  45958  limsupre3lem  45986  climuzlem  45997  xlimbr  46081  fourierdlem103  46463  fourierdlem104  46464  qndenserrnbllem  46548  2reuimp  47371  ralralimp  47534