Theorem infeq1d 9472

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

Syntax hints:   → wi 4   = wceq 1542  infcinf 9436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-sup 9437  df-inf 9438

This theorem is referenced by:  limsupval  15418  lcmval  16529  lcmass  16551  lcmfval  16558  lcmf0val  16559  lcmfpr  16564  odzval  16724  ramval  16941  imasval  17457  imasdsval  17461  gexval  19446  nmofval  24231  nmoval  24232  metdsval  24363  lebnumlem1  24477  lebnumlem3  24479  ovolval  24990  ovolshft  25028  ioorf  25090  mbflimsup  25183  ig1pval  25690  elqaalem1  25832  elqaalem2  25833  elqaalem3  25834  elqaa  25835  omsval  33292  omsfval  33293  ballotlemi  33499  pellfundval  41618  dgraaval  41886  supminfrnmpt  44155  infxrpnf  44156  infxrpnf2  44173  supminfxr  44174  supminfxr2  44179  supminfxrrnmpt  44181  limsupval3  44408  limsupresre  44412  limsupresico  44416  limsuppnfdlem  44417  limsupvaluz  44424  limsupvaluzmpt  44433  liminfval  44475  liminfgval  44478  liminfval5  44481  limsupresxr  44482  liminfresxr  44483  liminfval2  44484  liminfresico  44487  liminf10ex  44490  liminfvalxr  44499  fourierdlem31  44854  ovnval  45257  ovnval2  45261  ovnval2b  45268  ovolval2  45360  ovnovollem3  45374  smfinf  45534  smfinfmpt  45535  prmdvdsfmtnof1  46255