Theorem ralimdv 3175

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  r19.21v  3186  ss2ralv  4079  poss  5609  sess1  5665  sess2  5666  riinint  5994  iinpreima  7102  dffo4  7137  dffo5  7138  isoini2  7375  tfindsg  7898  el2mpocsbcl  8126  xpord3inddlem  8195  iiner  8847  xpf1o  9205  dffi3  9500  brwdom3  9651  xpwdomg  9654  ttrclss  9789  bndrank  9910  cfub  10318  cff1  10327  cfflb  10328  cfslb2n  10337  cofsmo  10338  cfcoflem  10341  pwcfsdom  10652  fpwwe2lem12  10711  inawinalem  10758  grupr  10866  fsequb  14026  cau3lem  15403  caubnd2  15406  caubnd  15407  rlim2lt  15543  rlim3  15544  climshftlem  15620  climcau  15719  caucvgb  15728  serf0  15729  modfsummods  15841  cvgcmp  15864  mreriincl  17656  acsfn1c  17720  islss4  20983  riinopn  22935  fiinbas  22980  baspartn  22982  isclo2  23117  lmcls  23331  lmcnp  23333  isnrm3  23388  1stcelcls  23490  llyss  23508  nllyss  23509  ptpjpre1  23600  txlly  23665  txnlly  23666  tx1stc  23679  xkococnlem  23688  fbunfip  23898  filssufilg  23940  cnpflf2  24029  fcfnei  24064  isucn2  24309  rescncf  24942  lebnum  25015  cfilss  25323  fgcfil  25324  iscau4  25332  cmetcaulem  25341  caussi  25350  ovolunlem1  25551  ulmclm  26448  ulmcaulem  26455  ulmcau  26456  ulmss  26458  rlimcnp  27026  cxploglim  27039  2sqreunnlem2  27517  pntlemp  27672  nosupno  27766  nosupres  27770  noinfno  27781  noinfres  27785  sssslt2  27859  madebdayim  27944  madebdaylemold  27954  axcontlem4  29000  ewlkle  29641  uspgr2wlkeq  29682  umgrwlknloop  29685  wlkiswwlksupgr2  29910  3cyclfrgrrn2  30319  nmlnoubi  30828  lnon0  30830  disjpreima  32606  resspos  32939  resstos  32940  submarchi  33166  prmidl2  33434  crefss  33795  iccllysconn  35218  cvmlift2lem1  35270  dmopab3rexdif  35373  ss2mcls  35536  mclsax  35537  isinf2  37371  poimirlem25  37605  poimirlem27  37607  upixp  37689  caushft  37721  sstotbnd3  37736  totbndss  37737  unichnidl  37991  ispridl2  37998  elrfirn2  42652  mzpsubst  42704  eluzrabdioph  42762  neik0pk1imk0  44009  mnuop3d  44240  ismnushort  44270  limsupub  45625  limsupre3lem  45653  climuzlem  45664  xlimbr  45748  fourierdlem103  46130  fourierdlem104  46131  qndenserrnbllem  46215  2reuimp  47030  ralralimp  47193