Theorem infeq1i 9430

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

Syntax hints:   = wceq 1540  infcinf 9392

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-ss 3931  df-uni 4872  df-sup 9393  df-inf 9394

This theorem is referenced by:  infsn  9458  nninf  12888  nn0inf  12889  lcmcom  16563  lcmass  16584  lcmf0  16604  imasdsval2  17479  imasdsf1olem  24261  ftalem6  26988  aks4d1  42077  sticksstones2  42135  supminfxr2  45465  limsup0  45692  limsupvaluz  45706  limsupmnflem  45718  limsupvaluz2  45736  limsup10ex  45771  cnrefiisp  45828  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  elaa2  46232  etransc  46281  ioorrnopn  46303  ovnval2  46543  ovolval3  46645  vonioolem2  46679