Theorem ralimdv 3179

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

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

This theorem is used by:  r19.21v  3190  ralimdvv  3214  ss2ralv  3983  poss  5564  sess1  5619  sess2  5620  riinint  5958  iinpreima  7077  dffo4  7111  dffo5  7112  isoini2  7354  tfindsg  7879  el2mpocsbcl  8104  xpord3inddlem  8181  iiner  8821  xpf1o  9169  dffi3  9433  brwdom3  9586  xpwdomg  9589  ttrclss  9731  bndrank  9864  r1filimi  9913  cfub  10336  cff1  10346  cfflb  10347  cfslb2n  10356  cofsmo  10357  cfcoflem  10360  pwcfsdom  10678  fpwwe2lem12  10737  inawinalem  10784  grupr  10892  fsequb  14128  cau3lem  15534  caubnd2  15537  caubnd  15538  rlim2lt  15676  rlim3  15677  climshftlem  15753  climcau  15850  caucvgb  15859  serf0  15860  modfsummods  15972  cvgcmp  15995  mreriincl  17780  acsfn1c  17848  resspos  18615  resstos  18616  chnrss  18801  islss4  21249  unichnlidl  21528  prmidl2  21634  riinopn  23238  fiinbas  23282  baspartn  23284  isclo2  23418  lmcls  23632  lmcnp  23634  isnrm3  23689  1stcelcls  23792  llyss  23810  nllyss  23811  ptpjpre1  23902  txlly  23967  txnlly  23968  tx1stc  23981  xkococnlem  23990  fbunfip  24200  filssufilg  24242  cnpflf2  24331  fcfnei  24366  isucn2  24609  rescncf  25230  lebnum  25297  cfilss  25603  fgcfil  25604  iscau4  25612  cmetcaulem  25621  caussi  25630  ovolunlem1  25830  ulmclm  26726  ulmcaulem  26733  ulmcau  26734  ulmss  26736  rlimcnp  27305  cxploglim  27317  2sqreunnlem2  27794  pntlemp  27949  nosupno  28072  nosupres  28076  noinfno  28087  noinfres  28091  ssslts2  28172  madebdayim  28286  madebdaylemold  28296  axcontlem4  29557  ewlkle  30198  uspgr2wlkeq  30238  umgrwlknloop  30241  wlkiswwlksupgr2  30478  3cyclfrgrrn2  30900  nmlnoubi  31410  lnon0  31412  disjpreima  33232  submarchi  33800  crefss  34534  iccllysconn  36136  cvmlift2lem1  36188  dmopab3rexdif  36291  ss2mcls  36454  mclsax  36455  dfttc4lem2  37444  isinf2  38468  poimirlem25  38703  poimirlem27  38705  upixp  38803  caushft  38835  sstotbnd3  38850  totbndss  38851  unichnidl  39105  ispridl2  39112  elrfirn2  43847  mzpsubst  43899  eluzrabdioph  43953  neik0pk1imk0  45187  mnuop3d  45395  ismnushort  45425  pwclaxpow  46113  limsupub  46853  limsupre3lem  46881  climuzlem  46892  xlimbr  46976  fourierdlem103  47358  fourierdlem104  47359  qndenserrnbllem  47443  2reuimp  48325  ralralimp  48487