Theorem infeq1d 9371

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

Syntax hints:   → wi 4   = wceq 1541  infcinf 9334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-ss 3915  df-uni 4861  df-sup 9335  df-inf 9336

This theorem is referenced by:  limsupval  15385  lcmval  16507  lcmass  16529  lcmfval  16536  lcmf0val  16537  lcmfpr  16542  odzval  16707  ramval  16924  imasval  17419  imasdsval  17423  gexval  19494  nmofval  24632  nmoval  24633  metdsval  24766  lebnumlem1  24890  lebnumlem3  24892  ovolval  25404  ovolshft  25442  ioorf  25504  mbflimsup  25597  ig1pval  26111  elqaalem1  26257  elqaalem2  26258  elqaalem3  26259  elqaa  26260  omsval  34329  omsfval  34330  ballotlemi  34537  pellfundval  43000  dgraaval  43264  supminfrnmpt  45570  infxrpnf  45571  infxrpnf2  45588  supminfxr  45589  supminfxr2  45594  supminfxrrnmpt  45596  limsupval3  45817  limsupresre  45821  limsupresico  45825  limsuppnfdlem  45826  limsupvaluz  45833  limsupvaluzmpt  45842  liminfval  45884  liminfgval  45887  liminfval5  45890  limsupresxr  45891  liminfresxr  45892  liminfval2  45893  liminfresico  45896  liminf10ex  45899  liminfvalxr  45908  fourierdlem31  46263  ovnval  46666  ovnval2  46670  ovnval2b  46677  ovolval2  46769  ovnovollem3  46783  smfinf  46943  smfinfmpt  46944  prmdvdsfmtnof1  47714