Theorem infeq1i 8624

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

Syntax hints:   = wceq 1653  infcinf 8587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-uni 4627  df-sup 8588  df-inf 8589

This theorem is referenced by:  infsn  8650  nninf  12010  nn0inf  12011  lcmcom  15637  lcmass  15658  lcmf0  15678  imasdsval2  16487  imasdsf1olem  22502  ftalem6  25152  supminfxr2  40429  limsup0  40657  limsupvaluz  40671  limsupmnflem  40683  limsupvaluz2  40701  limsup10ex  40736  cnrefiisp  40787  ioodvbdlimc1lem2  40878  ioodvbdlimc2lem  40880  elaa2  41181  etransc  41230  ioorrnopn  41255  ovnval2  41492  ovolval3  41594  vonioolem2  41628