Theorem infeq1d 9426

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

Syntax hints:   → wi 4   = wceq 1563  infcinf 9389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-ss 3924  df-uni 4868  df-sup 9390  df-inf 9391

This theorem is referenced by:  limsupval  15513  lcmval  16638  lcmass  16660  lcmfval  16667  lcmf0val  16668  lcmfpr  16673  odzval  16839  ramval  17056  imasval  17553  imasdsval  17557  gexval  19636  nmofval  24828  nmoval  24829  metdsval  24962  lebnumlem1  25077  lebnumlem3  25079  ovolval  25589  ovolshft  25627  ioorf  25689  mbflimsup  25782  ig1pval  26290  elqaalem1  26437  elqaalem2  26438  elqaalem3  26439  elqaa  26440  omsval  34595  omsfval  34596  ballotlemi  34803  pellfundval  43464  dgraaval  43728  supminfrnmpt  46018  infxrpnf  46019  infxrpnf2  46036  supminfxr  46037  supminfxr2  46042  supminfxrrnmpt  46044  limsupval3  46265  limsupresre  46269  limsupresico  46273  limsuppnfdlem  46274  limsupvaluz  46281  limsupvaluzmpt  46290  liminfval  46332  liminfgval  46335  liminfval5  46338  limsupresxr  46339  liminfresxr  46340  liminfval2  46341  liminfresico  46344  liminf10ex  46347  liminfvalxr  46356  fourierdlem31  46711  ovnval  47114  ovnval2  47118  ovnval2b  47125  ovolval2  47217  ovnovollem3  47231  smfinf  47391  smfinfmpt  47392  prmdvdsfmtnof1  48195