Theorem infeq1d 9393

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

Syntax hints:   → wi 4   = wceq 1542  infcinf 9356

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 9357  df-inf 9358

This theorem is referenced by:  limsupval  15409  lcmval  16531  lcmass  16553  lcmfval  16560  lcmf0val  16561  lcmfpr  16566  odzval  16731  ramval  16948  imasval  17444  imasdsval  17448  gexval  19519  nmofval  24670  nmoval  24671  metdsval  24804  lebnumlem1  24928  lebnumlem3  24930  ovolval  25442  ovolshft  25480  ioorf  25542  mbflimsup  25635  ig1pval  26149  elqaalem1  26295  elqaalem2  26296  elqaalem3  26297  elqaa  26298  omsval  34470  omsfval  34471  ballotlemi  34678  pellfundval  43234  dgraaval  43498  supminfrnmpt  45800  infxrpnf  45801  infxrpnf2  45818  supminfxr  45819  supminfxr2  45824  supminfxrrnmpt  45826  limsupval3  46047  limsupresre  46051  limsupresico  46055  limsuppnfdlem  46056  limsupvaluz  46063  limsupvaluzmpt  46072  liminfval  46114  liminfgval  46117  liminfval5  46120  limsupresxr  46121  liminfresxr  46122  liminfval2  46123  liminfresico  46126  liminf10ex  46129  liminfvalxr  46138  fourierdlem31  46493  ovnval  46896  ovnval2  46900  ovnval2b  46907  ovolval2  46999  ovnovollem3  47013  smfinf  47173  smfinfmpt  47174  prmdvdsfmtnof1  47944