Theorem infeq1i 9427

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

Syntax hints:   = wceq 1563  infcinf 9389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-ss 3924  df-uni 4868  df-sup 9390  df-inf 9391

This theorem is referenced by:  infsn  9455  nninf  12941  nn0inf  12942  lcmcom  16639  lcmass  16660  lcmf0  16680  imasdsval2  17558  imasdsf1olem  24487  ftalem6  27196  aks4d1  42713  sticksstones2  42771  supminfxr2  46042  limsup0  46267  limsupvaluz  46281  limsupmnflem  46293  limsupvaluz2  46311  limsup10ex  46346  cnrefiisp  46403  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  elaa2  46807  etransc  46856  ioorrnopn  46878  ovnval2  47118  ovolval3  47220  vonioolem2  47254