Theorem infeq1i 9167

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

Syntax hints:   = wceq 1539  infcinf 9130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-sup 9131  df-inf 9132

This theorem is referenced by:  infsn  9194  nninf  12598  nn0inf  12599  lcmcom  16226  lcmass  16247  lcmf0  16267  imasdsval2  17144  imasdsf1olem  23434  ftalem6  26132  aks4d1  40025  sticksstones2  40031  supminfxr2  42899  limsup0  43125  limsupvaluz  43139  limsupmnflem  43151  limsupvaluz2  43169  limsup10ex  43204  cnrefiisp  43261  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  elaa2  43665  etransc  43714  ioorrnopn  43736  ovnval2  43973  ovolval3  44075  vonioolem2  44109