Theorem infeq1d 9439

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

Syntax hints:   → wi 4   = wceq 1570  infcinf 9402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-ss 3923  df-uni 4874  df-sup 9403  df-inf 9404

This theorem is referenced by:  limsupval  15527  lcmval  16651  lcmass  16673  lcmfval  16680  lcmf0val  16681  lcmfpr  16686  odzval  16852  ramval  17069  imasval  17566  imasdsval  17570  gexval  19649  nmofval  24852  nmoval  24853  metdsval  24986  lebnumlem1  25101  lebnumlem3  25103  ovolval  25613  ovolshft  25651  ioorf  25713  mbflimsup  25806  ig1pval  26314  elqaalem1  26461  elqaalem2  26462  elqaalem3  26463  elqaa  26464  omsval  34664  omsfval  34665  ballotlemi  34872  pellfundval  43590  dgraaval  43854  supminfrnmpt  46142  infxrpnf  46143  infxrpnf2  46160  supminfxr  46161  supminfxr2  46166  supminfxrrnmpt  46168  limsupval3  46389  limsupresre  46393  limsupresico  46397  limsuppnfdlem  46398  limsupvaluz  46405  limsupvaluzmpt  46414  liminfval  46456  liminfgval  46459  liminfval5  46462  limsupresxr  46463  liminfresxr  46464  liminfval2  46465  liminfresico  46468  liminf10ex  46471  liminfvalxr  46480  fourierdlem31  46835  ovnval  47238  ovnval2  47242  ovnval2b  47249  ovolval2  47341  ovnovollem3  47355  smfinf  47515  smfinfmpt  47516  prmdvdsfmtnof1  48322