Theorem infeq1d 9166

Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)

Hypothesis

Ref	Expression
infeq1d.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
infeq1d	⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Proof of Theorem infeq1d

Step	Hyp	Ref	Expression
1		infeq1d.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
2		infeq1 9165	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1539  infcinf 9130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-sup 9131  df-inf 9132

This theorem is referenced by:  limsupval  15111  lcmval  16225  lcmass  16247  lcmfval  16254  lcmf0val  16255  lcmfpr  16260  odzval  16420  ramval  16637  imasval  17139  imasdsval  17143  gexval  19098  nmofval  23784  nmoval  23785  metdsval  23916  lebnumlem1  24030  lebnumlem3  24032  ovolval  24542  ovolshft  24580  ioorf  24642  mbflimsup  24735  ig1pval  25242  elqaalem1  25384  elqaalem2  25385  elqaalem3  25386  elqaa  25387  omsval  32160  omsfval  32161  ballotlemi  32367  pellfundval  40618  dgraaval  40885  supminfrnmpt  42875  infxrpnf  42876  infxrpnf2  42893  supminfxr  42894  supminfxr2  42899  supminfxrrnmpt  42901  limsupval3  43123  limsupresre  43127  limsupresico  43131  limsuppnfdlem  43132  limsupvaluz  43139  limsupvaluzmpt  43148  liminfval  43190  liminfgval  43193  liminfval5  43196  limsupresxr  43197  liminfresxr  43198  liminfval2  43199  liminfresico  43202  liminf10ex  43205  liminfvalxr  43214  fourierdlem31  43569  ovnval  43969  ovnval2  43973  ovnval2b  43980  ovolval2  44072  ovnovollem3  44086  smfinf  44238  smfinfmpt  44239  prmdvdsfmtnof1  44927