Theorem infeq1i 8552

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

Syntax hints:   = wceq 1632  infcinf 8515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-uni 4590  df-sup 8516  df-inf 8517

This theorem is referenced by:  infsn  8578  nninf  11983  nn0inf  11984  lcmcom  15529  lcmass  15550  lcmf0  15570  imasdsval2  16399  imasdsf1olem  22400  ftalem6  25025  supminfxr2  40216  limsup0  40448  limsupvaluz  40462  limsupmnflem  40474  limsupvaluz2  40492  limsup10ex  40527  cnrefiisp  40578  ioodvbdlimc1lem2  40669  ioodvbdlimc2lem  40671  elaa2  40973  etransc  41022  ioorrnopn  41047  ovnval2  41284  ovolval3  41386  vonioolem2  41420