Theorem infeq1d 9362

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

Syntax hints:   → wi 4   = wceq 1541  infcinf 9325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-ss 3919  df-uni 4860  df-sup 9326  df-inf 9327

This theorem is referenced by:  limsupval  15381  lcmval  16503  lcmass  16525  lcmfval  16532  lcmf0val  16533  lcmfpr  16538  odzval  16703  ramval  16920  imasval  17415  imasdsval  17419  gexval  19491  nmofval  24630  nmoval  24631  metdsval  24764  lebnumlem1  24888  lebnumlem3  24890  ovolval  25402  ovolshft  25440  ioorf  25502  mbflimsup  25595  ig1pval  26109  elqaalem1  26255  elqaalem2  26256  elqaalem3  26257  elqaa  26258  omsval  34304  omsfval  34305  ballotlemi  34512  pellfundval  42919  dgraaval  43183  supminfrnmpt  45489  infxrpnf  45490  infxrpnf2  45507  supminfxr  45508  supminfxr2  45513  supminfxrrnmpt  45515  limsupval3  45736  limsupresre  45740  limsupresico  45744  limsuppnfdlem  45745  limsupvaluz  45752  limsupvaluzmpt  45761  liminfval  45803  liminfgval  45806  liminfval5  45809  limsupresxr  45810  liminfresxr  45811  liminfval2  45812  liminfresico  45815  liminf10ex  45818  liminfvalxr  45827  fourierdlem31  46182  ovnval  46585  ovnval2  46589  ovnval2b  46596  ovolval2  46688  ovnovollem3  46702  smfinf  46862  smfinfmpt  46863  prmdvdsfmtnof1  47624