Theorem infeq1i 8795

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

Syntax hints:   = wceq 1525  infcinf 8758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ral 3112  df-rex 3113  df-rab 3116  df-uni 4752  df-sup 8759  df-inf 8760

This theorem is referenced by:  infsn  8822  nninf  12182  nn0inf  12183  lcmcom  15770  lcmass  15791  lcmf0  15811  imasdsval2  16622  imasdsf1olem  22670  ftalem6  25341  supminfxr2  41308  limsup0  41538  limsupvaluz  41552  limsupmnflem  41564  limsupvaluz2  41582  limsup10ex  41617  cnrefiisp  41674  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  elaa2  42083  etransc  42132  ioorrnopn  42154  ovnval2  42391  ovolval3  42493  vonioolem2  42527