Theorem infeq1i 9491

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

Syntax hints:   = wceq 1540  infcinf 9453

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-ss 3943  df-uni 4884  df-sup 9454  df-inf 9455

This theorem is referenced by:  infsn  9519  nninf  12945  nn0inf  12946  lcmcom  16612  lcmass  16633  lcmf0  16653  imasdsval2  17530  imasdsf1olem  24312  ftalem6  27040  aks4d1  42102  sticksstones2  42160  supminfxr2  45496  limsup0  45723  limsupvaluz  45737  limsupmnflem  45749  limsupvaluz2  45767  limsup10ex  45802  cnrefiisp  45859  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  elaa2  46263  etransc  46312  ioorrnopn  46334  ovnval2  46574  ovolval3  46676  vonioolem2  46710