Theorem infeq1d 9518

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

Syntax hints:   → wi 4   = wceq 1539  infcinf 9482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-ss 3967  df-uni 4907  df-sup 9483  df-inf 9484

This theorem is referenced by:  limsupval  15511  lcmval  16630  lcmass  16652  lcmfval  16659  lcmf0val  16660  lcmfpr  16665  odzval  16830  ramval  17047  imasval  17557  imasdsval  17561  gexval  19597  nmofval  24736  nmoval  24737  metdsval  24870  lebnumlem1  24994  lebnumlem3  24996  ovolval  25509  ovolshft  25547  ioorf  25609  mbflimsup  25702  ig1pval  26216  elqaalem1  26362  elqaalem2  26363  elqaalem3  26364  elqaa  26365  omsval  34296  omsfval  34297  ballotlemi  34504  pellfundval  42896  dgraaval  43161  supminfrnmpt  45461  infxrpnf  45462  infxrpnf2  45479  supminfxr  45480  supminfxr2  45485  supminfxrrnmpt  45487  limsupval3  45712  limsupresre  45716  limsupresico  45720  limsuppnfdlem  45721  limsupvaluz  45728  limsupvaluzmpt  45737  liminfval  45779  liminfgval  45782  liminfval5  45785  limsupresxr  45786  liminfresxr  45787  liminfval2  45788  liminfresico  45791  liminf10ex  45794  liminfvalxr  45803  fourierdlem31  46158  ovnval  46561  ovnval2  46565  ovnval2b  46572  ovolval2  46664  ovnovollem3  46678  smfinf  46838  smfinfmpt  46839  prmdvdsfmtnof1  47579