Theorem infeq1d 9454

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  infcinf 9417

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-ss 3916  df-uni 4868  df-sup 9418  df-inf 9419

This theorem is used by:  limsupval  15621  lcmval  16747  lcmass  16769  lcmfval  16776  lcmf0val  16777  lcmfpr  16782  odzval  16949  ramval  17166  imasval  17663  imasdsval  17667  gexval  19772  nmofval  25013  nmoval  25014  metdsval  25147  lebnumlem1  25262  lebnumlem3  25264  ovolval  25774  ovolshft  25812  ioorf  25874  mbflimsup  25967  ig1pval  26474  elqaalem1  26624  elqaalem2  26625  elqaalem3  26626  elqaa  26627  omsval  34908  omsfval  34909  ballotlemi  35116  pellfundval  43840  dgraaval  44104  supminfrnmpt  46399  infxrpnf  46400  infxrpnf2  46417  supminfxr  46418  supminfxr2  46423  supminfxrrnmpt  46425  limsupval3  46646  limsupresre  46650  limsupresico  46654  limsuppnfdlem  46655  limsupvaluz  46662  limsupvaluzmpt  46671  liminfval  46713  liminfgval  46716  liminfval5  46719  limsupresxr  46720  liminfresxr  46721  liminfval2  46722  liminfresico  46725  liminf10ex  46728  liminfvalxr  46737  fourierdlem31  47092  ovnval  47495  ovnval2  47499  ovnval2b  47506  ovolval2  47598  ovnovollem3  47612  smfinf  47772  smfinfmpt  47773  prmdvdsfmtnof1  48616