Theorem infeq1i 9418

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

Syntax hints:   = wceq 1559  infcinf 9380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-ss 3919  df-uni 4863  df-sup 9381  df-inf 9382

This theorem is referenced by:  infsn  9446  nninf  12923  nn0inf  12924  lcmcom  16617  lcmass  16638  lcmf0  16658  imasdsval2  17536  imasdsf1olem  24420  ftalem6  27129  aks4d1  42666  sticksstones2  42724  supminfxr2  46003  limsup0  46228  limsupvaluz  46242  limsupmnflem  46254  limsupvaluz2  46272  limsup10ex  46307  cnrefiisp  46364  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  elaa2  46768  etransc  46817  ioorrnopn  46839  ovnval2  47079  ovolval3  47181  vonioolem2  47215