Theorem infeq1d 9468

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

Syntax hints:   → wi 4   = wceq 1541  infcinf 9432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908  df-sup 9433  df-inf 9434

This theorem is referenced by:  limsupval  15414  lcmval  16525  lcmass  16547  lcmfval  16554  lcmf0val  16555  lcmfpr  16560  odzval  16720  ramval  16937  imasval  17453  imasdsval  17457  gexval  19440  nmofval  24222  nmoval  24223  metdsval  24354  lebnumlem1  24468  lebnumlem3  24470  ovolval  24981  ovolshft  25019  ioorf  25081  mbflimsup  25174  ig1pval  25681  elqaalem1  25823  elqaalem2  25824  elqaalem3  25825  elqaa  25826  omsval  33280  omsfval  33281  ballotlemi  33487  pellfundval  41603  dgraaval  41871  supminfrnmpt  44141  infxrpnf  44142  infxrpnf2  44159  supminfxr  44160  supminfxr2  44165  supminfxrrnmpt  44167  limsupval3  44394  limsupresre  44398  limsupresico  44402  limsuppnfdlem  44403  limsupvaluz  44410  limsupvaluzmpt  44419  liminfval  44461  liminfgval  44464  liminfval5  44467  limsupresxr  44468  liminfresxr  44469  liminfval2  44470  liminfresico  44473  liminf10ex  44476  liminfvalxr  44485  fourierdlem31  44840  ovnval  45243  ovnval2  45247  ovnval2b  45254  ovolval2  45346  ovnovollem3  45360  smfinf  45520  smfinfmpt  45521  prmdvdsfmtnof1  46241