Theorem infeq1i 9372

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

Syntax hints:   = wceq 1541  infcinf 9334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-ss 3915  df-uni 4861  df-sup 9335  df-inf 9336

This theorem is referenced by:  infsn  9400  nninf  12831  nn0inf  12832  lcmcom  16508  lcmass  16529  lcmf0  16549  imasdsval2  17424  imasdsf1olem  24291  ftalem6  27018  aks4d1  42205  sticksstones2  42263  supminfxr2  45594  limsup0  45819  limsupvaluz  45833  limsupmnflem  45845  limsupvaluz2  45863  limsup10ex  45898  cnrefiisp  45955  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  elaa2  46359  etransc  46408  ioorrnopn  46430  ovnval2  46670  ovolval3  46772  vonioolem2  46806