Theorem infeq1i 9473

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

Syntax hints:   = wceq 1542  infcinf 9436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-sup 9437  df-inf 9438

This theorem is referenced by:  infsn  9500  nninf  12913  nn0inf  12914  lcmcom  16530  lcmass  16551  lcmf0  16571  imasdsval2  17462  imasdsf1olem  23879  ftalem6  26582  aks4d1  40954  sticksstones2  40963  supminfxr2  44179  limsup0  44410  limsupvaluz  44424  limsupmnflem  44436  limsupvaluz2  44454  limsup10ex  44489  cnrefiisp  44546  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  elaa2  44950  etransc  44999  ioorrnopn  45021  ovnval2  45261  ovolval3  45363  vonioolem2  45397