Theorem infeq1i 9516

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

Syntax hints:   = wceq 1537  infcinf 9479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-ss 3980  df-uni 4913  df-sup 9480  df-inf 9481

This theorem is referenced by:  infsn  9543  nninf  12969  nn0inf  12970  lcmcom  16627  lcmass  16648  lcmf0  16668  imasdsval2  17563  imasdsf1olem  24399  ftalem6  27136  aks4d1  42071  sticksstones2  42129  supminfxr2  45419  limsup0  45650  limsupvaluz  45664  limsupmnflem  45676  limsupvaluz2  45694  limsup10ex  45729  cnrefiisp  45786  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  elaa2  46190  etransc  46239  ioorrnopn  46261  ovnval2  46501  ovolval3  46603  vonioolem2  46637