Theorem infeq1i 9392

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

Syntax hints:   = wceq 1542  infcinf 9354

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-ss 3906  df-uni 4851  df-sup 9355  df-inf 9356

This theorem is referenced by:  infsn  9420  nninf  12879  nn0inf  12880  lcmcom  16562  lcmass  16583  lcmf0  16603  imasdsval2  17480  imasdsf1olem  24338  ftalem6  27041  aks4d1  42528  sticksstones2  42586  supminfxr2  45897  limsup0  46122  limsupvaluz  46136  limsupmnflem  46148  limsupvaluz2  46166  limsup10ex  46201  cnrefiisp  46258  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  elaa2  46662  etransc  46711  ioorrnopn  46733  ovnval2  46973  ovolval3  47075  vonioolem2  47109