Theorem infeq1d 9474

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

Syntax hints:   → wi 4   = wceq 1539  infcinf 9438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-sup 9439  df-inf 9440

This theorem is referenced by:  limsupval  15422  lcmval  16533  lcmass  16555  lcmfval  16562  lcmf0val  16563  lcmfpr  16568  odzval  16728  ramval  16945  imasval  17461  imasdsval  17465  gexval  19487  nmofval  24451  nmoval  24452  metdsval  24583  lebnumlem1  24707  lebnumlem3  24709  ovolval  25222  ovolshft  25260  ioorf  25322  mbflimsup  25415  ig1pval  25925  elqaalem1  26068  elqaalem2  26069  elqaalem3  26070  elqaa  26071  omsval  33590  omsfval  33591  ballotlemi  33797  pellfundval  41920  dgraaval  42188  supminfrnmpt  44453  infxrpnf  44454  infxrpnf2  44471  supminfxr  44472  supminfxr2  44477  supminfxrrnmpt  44479  limsupval3  44706  limsupresre  44710  limsupresico  44714  limsuppnfdlem  44715  limsupvaluz  44722  limsupvaluzmpt  44731  liminfval  44773  liminfgval  44776  liminfval5  44779  limsupresxr  44780  liminfresxr  44781  liminfval2  44782  liminfresico  44785  liminf10ex  44788  liminfvalxr  44797  fourierdlem31  45152  ovnval  45555  ovnval2  45559  ovnval2b  45566  ovolval2  45658  ovnovollem3  45672  smfinf  45832  smfinfmpt  45833  prmdvdsfmtnof1  46553