Theorem infeq1d 8935

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

Syntax hints:   → wi 4   = wceq 1533  infcinf 8899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144  df-rab 3147  df-uni 4833  df-sup 8900  df-inf 8901

This theorem is referenced by:  limsupval  14825  lcmval  15930  lcmass  15952  lcmfval  15959  lcmf0val  15960  lcmfpr  15965  odzval  16122  ramval  16338  imasval  16778  imasdsval  16782  gexval  18697  nmofval  23317  nmoval  23318  metdsval  23449  lebnumlem1  23559  lebnumlem3  23561  ovolval  24068  ovolshft  24106  ioorf  24168  mbflimsup  24261  ig1pval  24760  elqaalem1  24902  elqaalem2  24903  elqaalem3  24904  elqaa  24905  omsval  31546  omsfval  31547  ballotlemi  31753  pellfundval  39470  dgraaval  39737  supminfrnmpt  41711  infxrpnf  41713  infxrpnf2  41731  supminfxr  41732  supminfxr2  41737  supminfxrrnmpt  41739  limsupval3  41965  limsupresre  41969  limsupresico  41973  limsuppnfdlem  41974  limsupvaluz  41981  limsupvaluzmpt  41990  liminfval  42032  liminfgval  42035  liminfval5  42038  limsupresxr  42039  liminfresxr  42040  liminfval2  42041  liminfresico  42044  liminf10ex  42047  liminfvalxr  42056  fourierdlem31  42416  ovnval  42816  ovnval2  42820  ovnval2b  42827  ovolval2  42919  ovnovollem3  42933  smfinf  43085  smfinfmpt  43086  prmdvdsfmtnof1  43742