Theorem infeq1d 9471

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

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

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 3915  df-uni 4868  df-sup 9435  df-inf 9436

This theorem is used by:  limsupval  15642  lcmval  16768  lcmass  16790  lcmfval  16797  lcmf0val  16798  lcmfpr  16803  odzval  16970  ramval  17187  imasval  17684  imasdsval  17688  gexval  19793  nmofval  25034  nmoval  25035  metdsval  25168  lebnumlem1  25283  lebnumlem3  25285  ovolval  25795  ovolshft  25833  ioorf  25895  mbflimsup  25988  ig1pval  26495  elqaalem1  26643  elqaalem2  26644  elqaalem3  26645  elqaa  26646  omsval  34926  omsfval  34927  ballotlemi  35134  frlmnzcoordval  43655  frlmnzcoordsca  43660  pellfundval  43888  dgraaval  44147  supminfrnmpt  46456  infxrpnf  46457  infxrpnf2  46474  supminfxr  46475  supminfxr2  46480  supminfxrrnmpt  46482  limsupval3  46703  limsupresre  46707  limsupresico  46711  limsuppnfdlem  46712  limsupvaluz  46719  limsupvaluzmpt  46728  liminfval  46770  liminfgval  46773  liminfval5  46776  limsupresxr  46777  liminfresxr  46778  liminfval2  46779  liminfresico  46782  liminf10ex  46785  liminfvalxr  46794  fourierdlem31  47149  ovnval  47552  ovnval2  47556  ovnval2b  47563  ovolval2  47655  ovnovollem3  47669  smfinf  47829  smfinfmpt  47830  prmdvdsfmtnof1  48673