Theorem infeq1d 9384

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

Syntax hints:   → wi 4   = wceq 1542  infcinf 9347

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-ss 3907  df-uni 4852  df-sup 9348  df-inf 9349

This theorem is referenced by:  limsupval  15427  lcmval  16552  lcmass  16574  lcmfval  16581  lcmf0val  16582  lcmfpr  16587  odzval  16753  ramval  16970  imasval  17466  imasdsval  17470  gexval  19544  nmofval  24689  nmoval  24690  metdsval  24823  lebnumlem1  24938  lebnumlem3  24940  ovolval  25450  ovolshft  25488  ioorf  25550  mbflimsup  25643  ig1pval  26151  elqaalem1  26296  elqaalem2  26297  elqaalem3  26298  elqaa  26299  omsval  34453  omsfval  34454  ballotlemi  34661  pellfundval  43326  dgraaval  43590  supminfrnmpt  45891  infxrpnf  45892  infxrpnf2  45909  supminfxr  45910  supminfxr2  45915  supminfxrrnmpt  45917  limsupval3  46138  limsupresre  46142  limsupresico  46146  limsuppnfdlem  46147  limsupvaluz  46154  limsupvaluzmpt  46163  liminfval  46205  liminfgval  46208  liminfval5  46211  limsupresxr  46212  liminfresxr  46213  liminfval2  46214  liminfresico  46217  liminf10ex  46220  liminfvalxr  46229  fourierdlem31  46584  ovnval  46987  ovnval2  46991  ovnval2b  46998  ovolval2  47090  ovnovollem3  47104  smfinf  47264  smfinfmpt  47265  prmdvdsfmtnof1  48062