Theorem infeq1d 9452

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-sup 9416  df-inf 9417

This theorem is used by:  limsupval  15565  lcmval  16688  lcmass  16710  lcmfval  16717  lcmf0val  16718  lcmfpr  16723  odzval  16889  ramval  17106  imasval  17603  imasdsval  17607  gexval  19711  nmofval  24946  nmoval  24947  metdsval  25080  lebnumlem1  25195  lebnumlem3  25197  ovolval  25707  ovolshft  25745  ioorf  25807  mbflimsup  25900  ig1pval  26408  elqaalem1  26558  elqaalem2  26559  elqaalem3  26560  elqaa  26561  omsval  34812  omsfval  34813  ballotlemi  35020  pellfundval  43729  dgraaval  43993  supminfrnmpt  46281  infxrpnf  46282  infxrpnf2  46299  supminfxr  46300  supminfxr2  46305  supminfxrrnmpt  46307  limsupval3  46528  limsupresre  46532  limsupresico  46536  limsuppnfdlem  46537  limsupvaluz  46544  limsupvaluzmpt  46553  liminfval  46595  liminfgval  46598  liminfval5  46601  limsupresxr  46602  liminfresxr  46603  liminfval2  46604  liminfresico  46607  liminf10ex  46610  liminfvalxr  46619  fourierdlem31  46974  ovnval  47377  ovnval2  47381  ovnval2b  47388  ovolval2  47480  ovnovollem3  47494  smfinf  47654  smfinfmpt  47655  prmdvdsfmtnof1  48498