Theorem infeq1d 8383

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

Syntax hints:   → wi 4   = wceq 1483  infcinf 8347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-uni 4437  df-sup 8348  df-inf 8349

This theorem is referenced by:  limsupval  14205  lcmval  15305  lcmass  15327  lcmfval  15334  lcmf0val  15335  lcmfpr  15340  odzval  15496  ramval  15712  imasval  16171  imasdsval  16175  gexval  17993  nmofval  22518  nmoval  22519  metdsval  22650  lebnumlem1  22760  lebnumlem3  22762  ovolval  23242  ovolshft  23279  ioorf  23341  mbflimsup  23433  ig1pval  23932  elqaalem1  24074  elqaalem2  24075  elqaalem3  24076  elqaa  24077  omsval  30355  omsfval  30356  ballotlemi  30562  pellfundval  37444  dgraaval  37714  supminfrnmpt  39672  infxrpnf  39674  infxrpnf2  39693  supminfxr  39694  supminfxr2  39699  supminfxrrnmpt  39701  limsupval3  39924  limsupresre  39928  limsupresico  39932  limsuppnfdlem  39933  limsupvaluz  39940  limsupvaluzmpt  39949  liminfval  39991  liminfgval  39994  liminfval5  39997  limsupresxr  39998  liminfresxr  39999  liminfval2  40000  liminfresico  40003  liminf10ex  40006  liminfvalxr  40015  fourierdlem31  40355  ovnval  40755  ovnval2  40759  ovnval2b  40766  ovolval2  40858  ovnovollem3  40872  smfinf  41024  smfinfmpt  41025  prmdvdsfmtnof1  41499