Theorem infeq1i 9547

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

Syntax hints:   = wceq 1537  infcinf 9510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-ss 3993  df-uni 4932  df-sup 9511  df-inf 9512

This theorem is referenced by:  infsn  9574  nninf  12994  nn0inf  12995  lcmcom  16640  lcmass  16661  lcmf0  16681  imasdsval2  17576  imasdsf1olem  24404  ftalem6  27139  aks4d1  42046  sticksstones2  42104  supminfxr2  45384  limsup0  45615  limsupvaluz  45629  limsupmnflem  45641  limsupvaluz2  45659  limsup10ex  45694  cnrefiisp  45751  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  elaa2  46155  etransc  46204  ioorrnopn  46226  ovnval2  46466  ovolval3  46568  vonioolem2  46602