Theorem infeq1d 9515

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 9514	. 2 ⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1537  infcinf 9479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-ss 3980  df-uni 4913  df-sup 9480  df-inf 9481

This theorem is referenced by:  limsupval  15507  lcmval  16626  lcmass  16648  lcmfval  16655  lcmf0val  16656  lcmfpr  16661  odzval  16825  ramval  17042  imasval  17558  imasdsval  17562  gexval  19611  nmofval  24751  nmoval  24752  metdsval  24883  lebnumlem1  25007  lebnumlem3  25009  ovolval  25522  ovolshft  25560  ioorf  25622  mbflimsup  25715  ig1pval  26230  elqaalem1  26376  elqaalem2  26377  elqaalem3  26378  elqaa  26379  omsval  34275  omsfval  34276  ballotlemi  34482  pellfundval  42868  dgraaval  43133  supminfrnmpt  45395  infxrpnf  45396  infxrpnf2  45413  supminfxr  45414  supminfxr2  45419  supminfxrrnmpt  45421  limsupval3  45648  limsupresre  45652  limsupresico  45656  limsuppnfdlem  45657  limsupvaluz  45664  limsupvaluzmpt  45673  liminfval  45715  liminfgval  45718  liminfval5  45721  limsupresxr  45722  liminfresxr  45723  liminfval2  45724  liminfresico  45727  liminf10ex  45730  liminfvalxr  45739  fourierdlem31  46094  ovnval  46497  ovnval2  46501  ovnval2b  46508  ovolval2  46600  ovnovollem3  46614  smfinf  46774  smfinfmpt  46775  prmdvdsfmtnof1  47512