Theorem infeq1i 9475

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

Syntax hints:   = wceq 1541  infcinf 9438

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-sup 9439  df-inf 9440

This theorem is referenced by:  infsn  9502  nninf  12917  nn0inf  12918  lcmcom  16534  lcmass  16555  lcmf0  16575  imasdsval2  17466  imasdsf1olem  24099  ftalem6  26806  aks4d1  41260  sticksstones2  41269  supminfxr2  44478  limsup0  44709  limsupvaluz  44723  limsupmnflem  44735  limsupvaluz2  44753  limsup10ex  44788  cnrefiisp  44845  ioodvbdlimc1lem2  44947  ioodvbdlimc2lem  44949  elaa2  45249  etransc  45298  ioorrnopn  45320  ovnval2  45560  ovolval3  45662  vonioolem2  45696