Theorem infeq1d 9429

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

Syntax hints:   → wi 4   = wceq 1540  infcinf 9392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-ss 3931  df-uni 4872  df-sup 9393  df-inf 9394

This theorem is referenced by:  limsupval  15440  lcmval  16562  lcmass  16584  lcmfval  16591  lcmf0val  16592  lcmfpr  16597  odzval  16762  ramval  16979  imasval  17474  imasdsval  17478  gexval  19508  nmofval  24602  nmoval  24603  metdsval  24736  lebnumlem1  24860  lebnumlem3  24862  ovolval  25374  ovolshft  25412  ioorf  25474  mbflimsup  25567  ig1pval  26081  elqaalem1  26227  elqaalem2  26228  elqaalem3  26229  elqaa  26230  omsval  34284  omsfval  34285  ballotlemi  34492  pellfundval  42868  dgraaval  43133  supminfrnmpt  45441  infxrpnf  45442  infxrpnf2  45459  supminfxr  45460  supminfxr2  45465  supminfxrrnmpt  45467  limsupval3  45690  limsupresre  45694  limsupresico  45698  limsuppnfdlem  45699  limsupvaluz  45706  limsupvaluzmpt  45715  liminfval  45757  liminfgval  45760  liminfval5  45763  limsupresxr  45764  liminfresxr  45765  liminfval2  45766  liminfresico  45769  liminf10ex  45772  liminfvalxr  45781  fourierdlem31  46136  ovnval  46539  ovnval2  46543  ovnval2b  46550  ovolval2  46642  ovnovollem3  46656  smfinf  46816  smfinfmpt  46817  prmdvdsfmtnof1  47585