Theorem infeq1d 9391

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

Syntax hints:   → wi 4   = wceq 1542  infcinf 9354

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-ss 3906  df-uni 4851  df-sup 9355  df-inf 9356

This theorem is referenced by:  limsupval  15436  lcmval  16561  lcmass  16583  lcmfval  16590  lcmf0val  16591  lcmfpr  16596  odzval  16762  ramval  16979  imasval  17475  imasdsval  17479  gexval  19553  nmofval  24679  nmoval  24680  metdsval  24813  lebnumlem1  24928  lebnumlem3  24930  ovolval  25440  ovolshft  25478  ioorf  25540  mbflimsup  25633  ig1pval  26141  elqaalem1  26285  elqaalem2  26286  elqaalem3  26287  elqaa  26288  omsval  34437  omsfval  34438  ballotlemi  34645  pellfundval  43308  dgraaval  43572  supminfrnmpt  45873  infxrpnf  45874  infxrpnf2  45891  supminfxr  45892  supminfxr2  45897  supminfxrrnmpt  45899  limsupval3  46120  limsupresre  46124  limsupresico  46128  limsuppnfdlem  46129  limsupvaluz  46136  limsupvaluzmpt  46145  liminfval  46187  liminfgval  46190  liminfval5  46193  limsupresxr  46194  liminfresxr  46195  liminfval2  46196  liminfresico  46199  liminf10ex  46202  liminfvalxr  46211  fourierdlem31  46566  ovnval  46969  ovnval2  46973  ovnval2b  46980  ovolval2  47072  ovnovollem3  47086  smfinf  47246  smfinfmpt  47247  prmdvdsfmtnof1  48050