Theorem ralimdv 3181

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3082

This theorem is used by:  r19.21v  3192  ralimdvv  3216  ss2ralv  4009  poss  5573  sess1  5628  sess2  5629  riinint  5964  iinpreima  7068  dffo4  7102  dffo5  7103  isoini2  7346  tfindsg  7863  el2mpocsbcl  8086  xpord3inddlem  8156  iiner  8793  xpf1o  9134  dffi3  9398  brwdom3  9551  xpwdomg  9554  ttrclss  9696  bndrank  9820  cfub  10247  cff1  10257  cfflb  10258  cfslb2n  10267  cofsmo  10268  cfcoflem  10271  pwcfsdom  10585  fpwwe2lem12  10644  inawinalem  10691  grupr  10799  fsequb  14031  cau3lem  15432  caubnd2  15435  caubnd  15436  rlim2lt  15574  rlim3  15575  climshftlem  15651  climcau  15748  caucvgb  15757  serf0  15758  modfsummods  15870  cvgcmp  15893  mreriincl  17674  acsfn1c  17742  resspos  18509  resstos  18510  chnrss  18695  islss4  21135  unichnlidl  21414  prmidl2  21518  riinopn  23117  fiinbas  23161  baspartn  23163  isclo2  23297  lmcls  23511  lmcnp  23513  isnrm3  23568  1stcelcls  23671  llyss  23689  nllyss  23690  ptpjpre1  23781  txlly  23846  txnlly  23847  tx1stc  23860  xkococnlem  23869  fbunfip  24079  filssufilg  24121  cnpflf2  24210  fcfnei  24245  isucn2  24488  rescncf  25109  lebnum  25176  cfilss  25482  fgcfil  25483  iscau4  25491  cmetcaulem  25500  caussi  25509  ovolunlem1  25709  ulmclm  26603  ulmcaulem  26610  ulmcau  26611  ulmss  26613  rlimcnp  27183  cxploglim  27195  2sqreunnlem2  27672  pntlemp  27827  nosupno  27920  nosupres  27924  noinfno  27935  noinfres  27939  ssslts2  28020  madebdayim  28134  madebdaylemold  28144  axcontlem4  29374  ewlkle  30015  uspgr2wlkeq  30055  umgrwlknloop  30058  wlkiswwlksupgr2  30295  3cyclfrgrrn2  30711  nmlnoubi  31221  lnon0  31223  disjpreima  33002  submarchi  33572  crefss  34305  r1filimi  35557  iccllysconn  35781  cvmlift2lem1  35833  dmopab3rexdif  35936  ss2mcls  36099  mclsax  36100  dfttc4lem2  37099  isinf2  38110  poimirlem25  38355  poimirlem27  38357  upixp  38440  caushft  38472  sstotbnd3  38487  totbndss  38488  unichnidl  38742  ispridl2  38749  elrfirn2  43487  mzpsubst  43539  eluzrabdioph  43593  neik0pk1imk0  44833  mnuop3d  45041  ismnushort  45071  pwclaxpow  45753  limsupub  46478  limsupre3lem  46506  climuzlem  46517  xlimbr  46601  fourierdlem103  46983  fourierdlem104  46984  qndenserrnbllem  47068  2reuimp  47912  ralralimp  48075