Theorem infeq1i 9518

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

Syntax hints:   = wceq 1540  infcinf 9481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-uni 4908  df-sup 9482  df-inf 9483

This theorem is referenced by:  infsn  9545  nninf  12971  nn0inf  12972  lcmcom  16630  lcmass  16651  lcmf0  16671  imasdsval2  17561  imasdsf1olem  24383  ftalem6  27121  aks4d1  42090  sticksstones2  42148  supminfxr2  45480  limsup0  45709  limsupvaluz  45723  limsupmnflem  45735  limsupvaluz2  45753  limsup10ex  45788  cnrefiisp  45845  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  elaa2  46249  etransc  46298  ioorrnopn  46320  ovnval2  46560  ovolval3  46662  vonioolem2  46696