Theorem infeq1i 9388

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

Syntax hints:   = wceq 1540  infcinf 9350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-ss 3922  df-uni 4862  df-sup 9351  df-inf 9352

This theorem is referenced by:  infsn  9416  nninf  12848  nn0inf  12849  lcmcom  16522  lcmass  16543  lcmf0  16563  imasdsval2  17438  imasdsf1olem  24277  ftalem6  27004  aks4d1  42065  sticksstones2  42123  supminfxr2  45452  limsup0  45679  limsupvaluz  45693  limsupmnflem  45705  limsupvaluz2  45723  limsup10ex  45758  cnrefiisp  45815  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  elaa2  46219  etransc  46268  ioorrnopn  46290  ovnval2  46530  ovolval3  46632  vonioolem2  46666