Theorem infeq1i 9385

Description: Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)

Hypothesis

Ref	Expression
infeq1i.1	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
infeq1i	⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Proof of Theorem infeq1i

Step	Hyp	Ref	Expression
1		infeq1i.1	. 2 ⊢ 𝐵 = 𝐶
2		infeq1 9383	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	ax-mp 5	1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Syntax hints:   = wceq 1542  infcinf 9347

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 3391  df-v 3432  df-ss 3907  df-uni 4852  df-sup 9348  df-inf 9349

This theorem is referenced by:  infsn  9413  nninf  12870  nn0inf  12871  lcmcom  16553  lcmass  16574  lcmf0  16594  imasdsval2  17471  imasdsf1olem  24348  ftalem6  27055  aks4d1  42542  sticksstones2  42600  supminfxr2  45915  limsup0  46140  limsupvaluz  46154  limsupmnflem  46166  limsupvaluz2  46184  limsup10ex  46219  cnrefiisp  46276  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  elaa2  46680  etransc  46729  ioorrnopn  46751  ovnval2  46991  ovolval3  47093  vonioolem2  47127