Theorem infeq1d 8925

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

Syntax hints:   → wi 4   = wceq 1538  infcinf 8889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-sup 8890  df-inf 8891

This theorem is referenced by:  limsupval  14823  lcmval  15926  lcmass  15948  lcmfval  15955  lcmf0val  15956  lcmfpr  15961  odzval  16118  ramval  16334  imasval  16776  imasdsval  16780  gexval  18695  nmofval  23320  nmoval  23321  metdsval  23452  lebnumlem1  23566  lebnumlem3  23568  ovolval  24077  ovolshft  24115  ioorf  24177  mbflimsup  24270  ig1pval  24773  elqaalem1  24915  elqaalem2  24916  elqaalem3  24917  elqaa  24918  omsval  31661  omsfval  31662  ballotlemi  31868  pellfundval  39821  dgraaval  40088  supminfrnmpt  42082  infxrpnf  42084  infxrpnf2  42102  supminfxr  42103  supminfxr2  42108  supminfxrrnmpt  42110  limsupval3  42334  limsupresre  42338  limsupresico  42342  limsuppnfdlem  42343  limsupvaluz  42350  limsupvaluzmpt  42359  liminfval  42401  liminfgval  42404  liminfval5  42407  limsupresxr  42408  liminfresxr  42409  liminfval2  42410  liminfresico  42413  liminf10ex  42416  liminfvalxr  42425  fourierdlem31  42780  ovnval  43180  ovnval2  43184  ovnval2b  43191  ovolval2  43283  ovnovollem3  43297  smfinf  43449  smfinfmpt  43450  prmdvdsfmtnof1  44104