Theorem ralimdv 3152

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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3150	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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 1912

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

This theorem is referenced by:  r19.21v  3163  ralimdvv  3187  ss2ralv  3993  poss  5535  sess1  5590  sess2  5591  riinint  5922  iinpreima  7016  dffo4  7050  dffo5  7051  isoini2  7288  tfindsg  7806  el2mpocsbcl  8029  xpord3inddlem  8098  iiner  8730  xpf1o  9071  dffi3  9338  brwdom3  9491  xpwdomg  9494  ttrclss  9635  bndrank  9759  cfub  10165  cff1  10174  cfflb  10175  cfslb2n  10184  cofsmo  10185  cfcoflem  10188  pwcfsdom  10500  fpwwe2lem12  10559  inawinalem  10606  grupr  10714  fsequb  13931  cau3lem  15311  caubnd2  15314  caubnd  15315  rlim2lt  15453  rlim3  15454  climshftlem  15530  climcau  15627  caucvgb  15636  serf0  15637  modfsummods  15750  cvgcmp  15773  mreriincl  17554  acsfn1c  17622  resspos  18389  resstos  18390  chnrss  18575  islss4  20951  riinopn  22886  fiinbas  22930  baspartn  22932  isclo2  23066  lmcls  23280  lmcnp  23282  isnrm3  23337  1stcelcls  23439  llyss  23457  nllyss  23458  ptpjpre1  23549  txlly  23614  txnlly  23615  tx1stc  23628  xkococnlem  23637  fbunfip  23847  filssufilg  23889  cnpflf2  23978  fcfnei  24013  isucn2  24256  rescncf  24877  lebnum  24944  cfilss  25250  fgcfil  25251  iscau4  25259  cmetcaulem  25268  caussi  25277  ovolunlem1  25477  ulmclm  26368  ulmcaulem  26375  ulmcau  26376  ulmss  26378  rlimcnp  26945  cxploglim  26958  2sqreunnlem2  27435  pntlemp  27590  nosupno  27684  nosupres  27688  noinfno  27699  noinfres  27703  ssslts2  27783  madebdayim  27897  madebdaylemold  27907  axcontlem4  29053  ewlkle  29692  uspgr2wlkeq  29732  umgrwlknloop  29735  wlkiswwlksupgr2  29963  3cyclfrgrrn2  30375  nmlnoubi  30885  lnon0  30887  disjpreima  32672  submarchi  33265  prmidl2  33519  crefss  34012  r1filimi  35265  iccllysconn  35451  cvmlift2lem1  35503  dmopab3rexdif  35606  ss2mcls  35769  mclsax  35770  dfttc4lem2  36730  isinf2  37738  poimirlem25  37983  poimirlem27  37985  upixp  38067  caushft  38099  sstotbnd3  38114  totbndss  38115  unichnidl  38369  ispridl2  38376  elrfirn2  43145  mzpsubst  43197  eluzrabdioph  43255  neik0pk1imk0  44495  mnuop3d  44719  ismnushort  44749  pwclaxpow  45432  limsupub  46153  limsupre3lem  46181  climuzlem  46192  xlimbr  46276  fourierdlem103  46658  fourierdlem104  46659  qndenserrnbllem  46743  2reuimp  47578  ralralimp  47741