Theorem infeq1d 8625

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

Syntax hints:   → wi 4   = wceq 1653  infcinf 8589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-uni 4629  df-sup 8590  df-inf 8591

This theorem is referenced by:  limsupval  14546  lcmval  15640  lcmass  15662  lcmfval  15669  lcmf0val  15670  lcmfpr  15675  odzval  15829  ramval  16045  imasval  16486  imasdsval  16490  gexval  18306  nmofval  22846  nmoval  22847  metdsval  22978  lebnumlem1  23088  lebnumlem3  23090  ovolval  23581  ovolshft  23619  ioorf  23681  mbflimsup  23774  ig1pval  24273  elqaalem1  24415  elqaalem2  24416  elqaalem3  24417  elqaa  24418  omsval  30871  omsfval  30872  ballotlemi  31079  pellfundval  38230  dgraaval  38499  supminfrnmpt  40415  infxrpnf  40417  infxrpnf2  40436  supminfxr  40437  supminfxr2  40442  supminfxrrnmpt  40444  limsupval3  40668  limsupresre  40672  limsupresico  40676  limsuppnfdlem  40677  limsupvaluz  40684  limsupvaluzmpt  40693  liminfval  40735  liminfgval  40738  liminfval5  40741  limsupresxr  40742  liminfresxr  40743  liminfval2  40744  liminfresico  40747  liminf10ex  40750  liminfvalxr  40759  fourierdlem31  41098  ovnval  41501  ovnval2  41505  ovnval2b  41512  ovolval2  41604  ovnovollem3  41618  smfinf  41770  smfinfmpt  41771  prmdvdsfmtnof1  42281