Theorem infeq1d 9500

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  infcinf 9463

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-uni 4871  df-sup 9464  df-inf 9465

This theorem is used by:  limsupval  15673  lcmval  16799  lcmass  16821  lcmfval  16828  lcmf0val  16829  lcmfpr  16834  odzval  17001  ramval  17218  imasval  17715  imasdsval  17719  gexval  19825  nmofval  25066  nmoval  25067  metdsval  25200  lebnumlem1  25315  lebnumlem3  25317  ovolval  25827  ovolshft  25865  ioorf  25927  mbflimsup  26020  ig1pval  26527  elqaalem1  26675  elqaalem2  26676  elqaalem3  26677  elqaa  26678  omsval  35008  omsfval  35009  ballotlemi  35216  frlmnzcoordval  43857  frlmnzcoordsca  43862  pellfundval  44091  dgraaval  44349  supminfrnmpt  46670  infxrpnf  46671  infxrpnf2  46688  supminfxr  46689  supminfxr2  46694  supminfxrrnmpt  46696  limsupval3  46917  limsupresre  46921  limsupresico  46925  limsuppnfdlem  46926  limsupvaluz  46933  limsupvaluzmpt  46942  liminfval  46984  liminfgval  46987  liminfval5  46990  limsupresxr  46991  liminfresxr  46992  liminfval2  46993  liminfresico  46996  liminf10ex  46999  liminfvalxr  47008  fourierdlem31  47363  ovnval  47766  ovnval2  47770  ovnval2b  47777  ovolval2  47869  ovnovollem3  47883  smfinf  48043  smfinfmpt  48044  prmdvdsfmtnof1  48887