Theorem infeq1i 9363

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 9361	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	ax-mp 5	1 ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Syntax hints:   = wceq 1541  infcinf 9325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-ss 3919  df-uni 4860  df-sup 9326  df-inf 9327

This theorem is referenced by:  infsn  9391  nninf  12827  nn0inf  12828  lcmcom  16504  lcmass  16525  lcmf0  16545  imasdsval2  17420  imasdsf1olem  24289  ftalem6  27016  aks4d1  42128  sticksstones2  42186  supminfxr2  45513  limsup0  45738  limsupvaluz  45752  limsupmnflem  45764  limsupvaluz2  45782  limsup10ex  45817  cnrefiisp  45874  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  elaa2  46278  etransc  46327  ioorrnopn  46349  ovnval2  46589  ovolval3  46691  vonioolem2  46725