Theorem infeq1d 9395

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

Syntax hints:   → wi 4   = wceq 1542  infcinf 9358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-ss 3920  df-uni 4866  df-sup 9359  df-inf 9360

This theorem is referenced by:  limsupval  15411  lcmval  16533  lcmass  16555  lcmfval  16562  lcmf0val  16563  lcmfpr  16568  odzval  16733  ramval  16950  imasval  17446  imasdsval  17450  gexval  19524  nmofval  24675  nmoval  24676  metdsval  24809  lebnumlem1  24933  lebnumlem3  24935  ovolval  25447  ovolshft  25485  ioorf  25547  mbflimsup  25640  ig1pval  26154  elqaalem1  26300  elqaalem2  26301  elqaalem3  26302  elqaa  26303  omsval  34477  omsfval  34478  ballotlemi  34685  pellfundval  43266  dgraaval  43530  supminfrnmpt  45832  infxrpnf  45833  infxrpnf2  45850  supminfxr  45851  supminfxr2  45856  supminfxrrnmpt  45858  limsupval3  46079  limsupresre  46083  limsupresico  46087  limsuppnfdlem  46088  limsupvaluz  46095  limsupvaluzmpt  46104  liminfval  46146  liminfgval  46149  liminfval5  46152  limsupresxr  46153  liminfresxr  46154  liminfval2  46155  liminfresico  46158  liminf10ex  46161  liminfvalxr  46170  fourierdlem31  46525  ovnval  46928  ovnval2  46932  ovnval2b  46939  ovolval2  47031  ovnovollem3  47045  smfinf  47205  smfinfmpt  47206  prmdvdsfmtnof1  47976