Theorem infeq1i 9382

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

Syntax hints:   = wceq 1541  infcinf 9344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-ss 3918  df-uni 4864  df-sup 9345  df-inf 9346

This theorem is referenced by:  infsn  9410  nninf  12842  nn0inf  12843  lcmcom  16520  lcmass  16541  lcmf0  16561  imasdsval2  17437  imasdsf1olem  24317  ftalem6  27044  aks4d1  42343  sticksstones2  42401  supminfxr2  45713  limsup0  45938  limsupvaluz  45952  limsupmnflem  45964  limsupvaluz2  45982  limsup10ex  46017  cnrefiisp  46074  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  elaa2  46478  etransc  46527  ioorrnopn  46549  ovnval2  46789  ovolval3  46891  vonioolem2  46925