Theorem ralimdv 3148

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1810). (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 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  r19.21v  3159  ralimdvv  3187  ss2ralv  4020  poss  5551  sess1  5606  sess2  5607  riinint  5938  iinpreima  7044  dffo4  7078  dffo5  7079  isoini2  7317  tfindsg  7840  el2mpocsbcl  8067  xpord3inddlem  8136  iiner  8765  xpf1o  9109  dffi3  9389  brwdom3  9542  xpwdomg  9545  ttrclss  9680  bndrank  9801  cfub  10209  cff1  10218  cfflb  10219  cfslb2n  10228  cofsmo  10229  cfcoflem  10232  pwcfsdom  10543  fpwwe2lem12  10602  inawinalem  10649  grupr  10757  fsequb  13947  cau3lem  15328  caubnd2  15331  caubnd  15332  rlim2lt  15470  rlim3  15471  climshftlem  15547  climcau  15644  caucvgb  15653  serf0  15654  modfsummods  15766  cvgcmp  15789  mreriincl  17566  acsfn1c  17630  islss4  20875  riinopn  22802  fiinbas  22846  baspartn  22848  isclo2  22982  lmcls  23196  lmcnp  23198  isnrm3  23253  1stcelcls  23355  llyss  23373  nllyss  23374  ptpjpre1  23465  txlly  23530  txnlly  23531  tx1stc  23544  xkococnlem  23553  fbunfip  23763  filssufilg  23805  cnpflf2  23894  fcfnei  23929  isucn2  24173  rescncf  24797  lebnum  24870  cfilss  25177  fgcfil  25178  iscau4  25186  cmetcaulem  25195  caussi  25204  ovolunlem1  25405  ulmclm  26303  ulmcaulem  26310  ulmcau  26311  ulmss  26313  rlimcnp  26882  cxploglim  26895  2sqreunnlem2  27373  pntlemp  27528  nosupno  27622  nosupres  27626  noinfno  27637  noinfres  27641  sssslt2  27715  madebdayim  27806  madebdaylemold  27816  axcontlem4  28901  ewlkle  29540  uspgr2wlkeq  29581  umgrwlknloop  29584  wlkiswwlksupgr2  29814  3cyclfrgrrn2  30223  nmlnoubi  30732  lnon0  30734  disjpreima  32520  resspos  32899  resstos  32900  submarchi  33147  prmidl2  33419  crefss  33846  iccllysconn  35244  cvmlift2lem1  35296  dmopab3rexdif  35399  ss2mcls  35562  mclsax  35563  isinf2  37400  poimirlem25  37646  poimirlem27  37648  upixp  37730  caushft  37762  sstotbnd3  37777  totbndss  37778  unichnidl  38032  ispridl2  38039  elrfirn2  42691  mzpsubst  42743  eluzrabdioph  42801  neik0pk1imk0  44043  mnuop3d  44267  ismnushort  44297  pwclaxpow  44981  limsupub  45709  limsupre3lem  45737  climuzlem  45748  xlimbr  45832  fourierdlem103  46214  fourierdlem104  46215  qndenserrnbllem  46299  2reuimp  47120  ralralimp  47283