Theorem infeq1d 9236

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 9235	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1539  infcinf 9200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-sup 9201  df-inf 9202

This theorem is referenced by:  limsupval  15183  lcmval  16297  lcmass  16319  lcmfval  16326  lcmf0val  16327  lcmfpr  16332  odzval  16492  ramval  16709  imasval  17222  imasdsval  17226  gexval  19183  nmofval  23878  nmoval  23879  metdsval  24010  lebnumlem1  24124  lebnumlem3  24126  ovolval  24637  ovolshft  24675  ioorf  24737  mbflimsup  24830  ig1pval  25337  elqaalem1  25479  elqaalem2  25480  elqaalem3  25481  elqaa  25482  omsval  32260  omsfval  32261  ballotlemi  32467  pellfundval  40702  dgraaval  40969  supminfrnmpt  42985  infxrpnf  42986  infxrpnf2  43003  supminfxr  43004  supminfxr2  43009  supminfxrrnmpt  43011  limsupval3  43233  limsupresre  43237  limsupresico  43241  limsuppnfdlem  43242  limsupvaluz  43249  limsupvaluzmpt  43258  liminfval  43300  liminfgval  43303  liminfval5  43306  limsupresxr  43307  liminfresxr  43308  liminfval2  43309  liminfresico  43312  liminf10ex  43315  liminfvalxr  43324  fourierdlem31  43679  ovnval  44079  ovnval2  44083  ovnval2b  44090  ovolval2  44182  ovnovollem3  44196  smfinf  44351  smfinfmpt  44352  prmdvdsfmtnof1  45039