Theorem infeq1i 9394

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

Syntax hints:   = wceq 1542  infcinf 9356

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 3402  df-v 3444  df-ss 3920  df-uni 4866  df-sup 9357  df-inf 9358

This theorem is referenced by:  infsn  9422  nninf  12854  nn0inf  12855  lcmcom  16532  lcmass  16553  lcmf0  16573  imasdsval2  17449  imasdsf1olem  24329  ftalem6  27056  aks4d1  42456  sticksstones2  42514  supminfxr2  45824  limsup0  46049  limsupvaluz  46063  limsupmnflem  46075  limsupvaluz2  46093  limsup10ex  46128  cnrefiisp  46185  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  elaa2  46589  etransc  46638  ioorrnopn  46660  ovnval2  46900  ovolval3  47002  vonioolem2  47036