Theorem infeq1i 9389

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

Syntax hints:   = wceq 1547  infcinf 9351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-ss 3907  df-uni 4846  df-sup 9352  df-inf 9353

This theorem is referenced by:  infsn  9417  nninf  12877  nn0inf  12878  lcmcom  16560  lcmass  16581  lcmf0  16601  imasdsval2  17478  imasdsf1olem  24363  ftalem6  27066  aks4d1  42581  sticksstones2  42639  supminfxr2  45919  limsup0  46144  limsupvaluz  46158  limsupmnflem  46170  limsupvaluz2  46188  limsup10ex  46223  cnrefiisp  46280  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  elaa2  46684  etransc  46733  ioorrnopn  46755  ovnval2  46995  ovolval3  47097  vonioolem2  47131