Theorem ralimdv 3165

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

Syntax hints:   → wi 4   ∈ wcel 2099  ∀wral 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3058

This theorem is referenced by:  r19.21v  3175  ss2ralv  4048  poss  5586  sess1  5640  sess2  5641  riinint  5965  iinpreima  7072  dffo4  7107  dffo5  7108  isoini2  7341  tfindsg  7859  el2mpocsbcl  8084  xpord3inddlem  8153  iiner  8801  xpf1o  9157  dffi3  9448  brwdom3  9599  xpwdomg  9602  ttrclss  9737  bndrank  9858  cfub  10266  cff1  10275  cfflb  10276  cfslb2n  10285  cofsmo  10286  cfcoflem  10289  pwcfsdom  10600  fpwwe2lem12  10659  inawinalem  10706  grupr  10814  fsequb  13966  cau3lem  15327  caubnd2  15330  caubnd  15331  rlim2lt  15467  rlim3  15468  climshftlem  15544  climcau  15643  caucvgb  15652  serf0  15653  modfsummods  15765  cvgcmp  15788  mreriincl  17571  acsfn1c  17635  islss4  20839  riinopn  22803  fiinbas  22848  baspartn  22850  isclo2  22985  lmcls  23199  lmcnp  23201  isnrm3  23256  1stcelcls  23358  llyss  23376  nllyss  23377  ptpjpre1  23468  txlly  23533  txnlly  23534  tx1stc  23547  xkococnlem  23556  fbunfip  23766  filssufilg  23808  cnpflf2  23897  fcfnei  23932  isucn2  24177  rescncf  24810  lebnum  24883  cfilss  25191  fgcfil  25192  iscau4  25200  cmetcaulem  25209  caussi  25218  ovolunlem1  25419  ulmclm  26316  ulmcaulem  26323  ulmcau  26324  ulmss  26326  rlimcnp  26890  cxploglim  26903  2sqreunnlem2  27381  pntlemp  27536  nosupno  27629  nosupres  27633  noinfno  27644  noinfres  27648  sssslt2  27722  madebdayim  27807  madebdaylemold  27817  axcontlem4  28771  ewlkle  29412  uspgr2wlkeq  29453  umgrwlknloop  29456  wlkiswwlksupgr2  29681  3cyclfrgrrn2  30090  nmlnoubi  30599  lnon0  30601  disjpreima  32367  resspos  32687  resstos  32688  submarchi  32888  prmidl2  33151  crefss  33444  iccllysconn  34854  cvmlift2lem1  34906  dmopab3rexdif  35009  ss2mcls  35172  mclsax  35173  isinf2  36878  poimirlem25  37112  poimirlem27  37114  upixp  37196  caushft  37228  sstotbnd3  37243  totbndss  37244  unichnidl  37498  ispridl2  37505  elrfirn2  42110  mzpsubst  42162  eluzrabdioph  42220  neik0pk1imk0  43471  mnuop3d  43702  ismnushort  43732  limsupub  45086  limsupre3lem  45114  climuzlem  45125  xlimbr  45209  fourierdlem103  45591  fourierdlem104  45592  qndenserrnbllem  45676  2reuimp  46489  ralralimp  46652