Theorem infeq1d 9448

Description: Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)

Hypothesis

Ref	Expression
infeq1d.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
infeq1d	⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Proof of Theorem infeq1d

Step	Hyp	Ref	Expression
1		infeq1d.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
2		infeq1 9447	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	syl 18	1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  infcinf 9411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-ss 3925  df-uni 4878  df-sup 9412  df-inf 9413

This theorem is used by:  limsupval  15551  lcmval  16675  lcmass  16697  lcmfval  16704  lcmf0val  16705  lcmfpr  16710  odzval  16876  ramval  17093  imasval  17590  imasdsval  17594  gexval  19679  nmofval  24908  nmoval  24909  metdsval  25042  lebnumlem1  25157  lebnumlem3  25159  ovolval  25669  ovolshft  25707  ioorf  25769  mbflimsup  25862  ig1pval  26370  elqaalem1  26517  elqaalem2  26518  elqaalem3  26519  elqaa  26520  omsval  34715  omsfval  34716  ballotlemi  34923  pellfundval  43648  dgraaval  43912  supminfrnmpt  46200  infxrpnf  46201  infxrpnf2  46218  supminfxr  46219  supminfxr2  46224  supminfxrrnmpt  46226  limsupval3  46447  limsupresre  46451  limsupresico  46455  limsuppnfdlem  46456  limsupvaluz  46463  limsupvaluzmpt  46472  liminfval  46514  liminfgval  46517  liminfval5  46520  limsupresxr  46521  liminfresxr  46522  liminfval2  46523  liminfresico  46526  liminf10ex  46529  liminfvalxr  46538  fourierdlem31  46893  ovnval  47296  ovnval2  47300  ovnval2b  47307  ovolval2  47399  ovnovollem3  47413  smfinf  47573  smfinfmpt  47574  prmdvdsfmtnof1  48380