Theorem infeq1i 9500

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

Syntax hints:   = wceq 1539  infcinf 9463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-ss 3948  df-uni 4888  df-sup 9464  df-inf 9465

This theorem is referenced by:  infsn  9527  nninf  12953  nn0inf  12954  lcmcom  16612  lcmass  16633  lcmf0  16653  imasdsval2  17532  imasdsf1olem  24328  ftalem6  27057  aks4d1  42049  sticksstones2  42107  supminfxr2  45437  limsup0  45666  limsupvaluz  45680  limsupmnflem  45692  limsupvaluz2  45710  limsup10ex  45745  cnrefiisp  45802  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  elaa2  46206  etransc  46255  ioorrnopn  46277  ovnval2  46517  ovolval3  46619  vonioolem2  46653