Theorem ralimdv 3179

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is referenced by:  r19.21v  3190  ralimdvv  3214  ss2ralv  4008  poss  5571  sess1  5626  sess2  5627  riinint  5962  iinpreima  7064  dffo4  7098  dffo5  7099  isoini2  7337  tfindsg  7853  el2mpocsbcl  8076  xpord3inddlem  8146  iiner  8783  xpf1o  9123  dffi3  9387  brwdom3  9540  xpwdomg  9543  ttrclss  9685  bndrank  9809  cfub  10227  cff1  10237  cfflb  10238  cfslb2n  10247  cofsmo  10248  cfcoflem  10251  pwcfsdom  10563  fpwwe2lem12  10622  inawinalem  10669  grupr  10777  fsequb  14007  cau3lem  15402  caubnd2  15405  caubnd  15406  rlim2lt  15544  rlim3  15545  climshftlem  15621  climcau  15718  caucvgb  15727  serf0  15728  modfsummods  15841  cvgcmp  15864  mreriincl  17645  acsfn1c  17713  resspos  18480  resstos  18481  chnrss  18666  islss4  21083  unichnlidl  21362  prmidl2  21466  riinopn  23065  fiinbas  23109  baspartn  23111  isclo2  23245  lmcls  23459  lmcnp  23461  isnrm3  23516  1stcelcls  23618  llyss  23636  nllyss  23637  ptpjpre1  23728  txlly  23793  txnlly  23794  tx1stc  23807  xkococnlem  23816  fbunfip  24026  filssufilg  24068  cnpflf2  24157  fcfnei  24192  isucn2  24435  rescncf  25056  lebnum  25123  cfilss  25429  fgcfil  25430  iscau4  25438  cmetcaulem  25447  caussi  25456  ovolunlem1  25656  ulmclm  26550  ulmcaulem  26557  ulmcau  26558  ulmss  26560  rlimcnp  27130  cxploglim  27142  2sqreunnlem2  27619  pntlemp  27774  nosupno  27867  nosupres  27871  noinfno  27882  noinfres  27886  ssslts2  27967  madebdayim  28081  madebdaylemold  28091  axcontlem4  29317  ewlkle  29955  uspgr2wlkeq  29995  umgrwlknloop  29998  wlkiswwlksupgr2  30226  3cyclfrgrrn2  30638  nmlnoubi  31148  lnon0  31150  disjpreima  32929  submarchi  33506  crefss  34239  r1filimi  35497  iccllysconn  35742  cvmlift2lem1  35794  dmopab3rexdif  35897  ss2mcls  36060  mclsax  36061  dfttc4lem2  37060  isinf2  38071  poimirlem25  38316  poimirlem27  38318  upixp  38400  caushft  38432  sstotbnd3  38447  totbndss  38448  unichnidl  38702  ispridl2  38709  elrfirn2  43447  mzpsubst  43499  eluzrabdioph  43553  neik0pk1imk0  44793  mnuop3d  45001  ismnushort  45031  pwclaxpow  45713  limsupub  46438  limsupre3lem  46466  climuzlem  46477  xlimbr  46561  fourierdlem103  46943  fourierdlem104  46944  qndenserrnbllem  47028  2reuimp  47872  ralralimp  48035