Theorem infeq1i 9437

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

Syntax hints:   = wceq 1540  infcinf 9399

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-ss 3934  df-uni 4875  df-sup 9400  df-inf 9401

This theorem is referenced by:  infsn  9465  nninf  12895  nn0inf  12896  lcmcom  16570  lcmass  16591  lcmf0  16611  imasdsval2  17486  imasdsf1olem  24268  ftalem6  26995  aks4d1  42084  sticksstones2  42142  supminfxr2  45472  limsup0  45699  limsupvaluz  45713  limsupmnflem  45725  limsupvaluz2  45743  limsup10ex  45778  cnrefiisp  45835  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  elaa2  46239  etransc  46288  ioorrnopn  46310  ovnval2  46550  ovolval3  46652  vonioolem2  46686