Theorem ralimdv 3148

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

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

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 3050

This theorem is referenced by:  r19.21v  3159  ralimdvv  3183  ss2ralv  4002  poss  5532  sess1  5587  sess2  5588  riinint  5919  iinpreima  7012  dffo4  7046  dffo5  7047  isoini2  7283  tfindsg  7801  el2mpocsbcl  8025  xpord3inddlem  8094  iiner  8724  xpf1o  9065  dffi3  9332  brwdom3  9485  xpwdomg  9488  ttrclss  9627  bndrank  9751  cfub  10157  cff1  10166  cfflb  10167  cfslb2n  10176  cofsmo  10177  cfcoflem  10180  pwcfsdom  10492  fpwwe2lem12  10551  inawinalem  10598  grupr  10706  fsequb  13896  cau3lem  15276  caubnd2  15279  caubnd  15280  rlim2lt  15418  rlim3  15419  climshftlem  15495  climcau  15592  caucvgb  15601  serf0  15602  modfsummods  15714  cvgcmp  15737  mreriincl  17515  acsfn1c  17583  resspos  18350  resstos  18351  chnrss  18536  islss4  20911  riinopn  22850  fiinbas  22894  baspartn  22896  isclo2  23030  lmcls  23244  lmcnp  23246  isnrm3  23301  1stcelcls  23403  llyss  23421  nllyss  23422  ptpjpre1  23513  txlly  23578  txnlly  23579  tx1stc  23592  xkococnlem  23601  fbunfip  23811  filssufilg  23853  cnpflf2  23942  fcfnei  23977  isucn2  24220  rescncf  24844  lebnum  24917  cfilss  25224  fgcfil  25225  iscau4  25233  cmetcaulem  25242  caussi  25251  ovolunlem1  25452  ulmclm  26350  ulmcaulem  26357  ulmcau  26358  ulmss  26360  rlimcnp  26929  cxploglim  26942  2sqreunnlem2  27420  pntlemp  27575  nosupno  27669  nosupres  27673  noinfno  27684  noinfres  27688  sssslt2  27764  madebdayim  27860  madebdaylemold  27870  axcontlem4  28989  ewlkle  29628  uspgr2wlkeq  29668  umgrwlknloop  29671  wlkiswwlksupgr2  29899  3cyclfrgrrn2  30311  nmlnoubi  30820  lnon0  30822  disjpreima  32608  submarchi  33217  prmidl2  33471  crefss  33955  r1filimi  35208  iccllysconn  35393  cvmlift2lem1  35445  dmopab3rexdif  35548  ss2mcls  35711  mclsax  35712  isinf2  37549  poimirlem25  37785  poimirlem27  37787  upixp  37869  caushft  37901  sstotbnd3  37916  totbndss  37917  unichnidl  38171  ispridl2  38178  elrfirn2  42880  mzpsubst  42932  eluzrabdioph  42990  neik0pk1imk0  44230  mnuop3d  44454  ismnushort  44484  pwclaxpow  45167  limsupub  45890  limsupre3lem  45918  climuzlem  45929  xlimbr  46013  fourierdlem103  46395  fourierdlem104  46396  qndenserrnbllem  46480  2reuimp  47303  ralralimp  47466