Theorem infeq1d 9546

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

Syntax hints:   → wi 4   = wceq 1537  infcinf 9510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-ss 3993  df-uni 4932  df-sup 9511  df-inf 9512

This theorem is referenced by:  limsupval  15520  lcmval  16639  lcmass  16661  lcmfval  16668  lcmf0val  16669  lcmfpr  16674  odzval  16838  ramval  17055  imasval  17571  imasdsval  17575  gexval  19620  nmofval  24756  nmoval  24757  metdsval  24888  lebnumlem1  25012  lebnumlem3  25014  ovolval  25527  ovolshft  25565  ioorf  25627  mbflimsup  25720  ig1pval  26235  elqaalem1  26379  elqaalem2  26380  elqaalem3  26381  elqaa  26382  omsval  34258  omsfval  34259  ballotlemi  34465  pellfundval  42836  dgraaval  43101  supminfrnmpt  45360  infxrpnf  45361  infxrpnf2  45378  supminfxr  45379  supminfxr2  45384  supminfxrrnmpt  45386  limsupval3  45613  limsupresre  45617  limsupresico  45621  limsuppnfdlem  45622  limsupvaluz  45629  limsupvaluzmpt  45638  liminfval  45680  liminfgval  45683  liminfval5  45686  limsupresxr  45687  liminfresxr  45688  liminfval2  45689  liminfresico  45692  liminf10ex  45695  liminfvalxr  45704  fourierdlem31  46059  ovnval  46462  ovnval2  46466  ovnval2b  46473  ovolval2  46565  ovnovollem3  46579  smfinf  46739  smfinfmpt  46740  prmdvdsfmtnof1  47461