Theorem infeq1i 9386

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

Syntax hints:   = wceq 1548  infcinf 9348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-ss 3901  df-uni 4841  df-sup 9349  df-inf 9350

This theorem is referenced by:  infsn  9414  nninf  12874  nn0inf  12875  lcmcom  16557  lcmass  16578  lcmf0  16598  imasdsval2  17475  imasdsf1olem  24359  ftalem6  27062  aks4d1  42587  sticksstones2  42645  supminfxr2  45924  limsup0  46149  limsupvaluz  46163  limsupmnflem  46175  limsupvaluz2  46193  limsup10ex  46228  cnrefiisp  46285  ioodvbdlimc1lem2  46387  ioodvbdlimc2lem  46389  elaa2  46689  etransc  46738  ioorrnopn  46760  ovnval2  47000  ovolval3  47102  vonioolem2  47136