Theorem infeq1d 8671

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

Syntax hints:   → wi 4   = wceq 1601  infcinf 8635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-ral 3095  df-rex 3096  df-rab 3099  df-uni 4672  df-sup 8636  df-inf 8637

This theorem is referenced by:  limsupval  14613  lcmval  15711  lcmass  15733  lcmfval  15740  lcmf0val  15741  lcmfpr  15746  odzval  15900  ramval  16116  imasval  16557  imasdsval  16561  gexval  18377  nmofval  22926  nmoval  22927  metdsval  23058  lebnumlem1  23168  lebnumlem3  23170  ovolval  23677  ovolshft  23715  ioorf  23777  mbflimsup  23870  ig1pval  24369  elqaalem1  24511  elqaalem2  24512  elqaalem3  24513  elqaa  24514  omsval  30953  omsfval  30954  ballotlemi  31161  pellfundval  38404  dgraaval  38673  supminfrnmpt  40578  infxrpnf  40580  infxrpnf2  40598  supminfxr  40599  supminfxr2  40604  supminfxrrnmpt  40606  limsupval3  40832  limsupresre  40836  limsupresico  40840  limsuppnfdlem  40841  limsupvaluz  40848  limsupvaluzmpt  40857  liminfval  40899  liminfgval  40902  liminfval5  40905  limsupresxr  40906  liminfresxr  40907  liminfval2  40908  liminfresico  40911  liminf10ex  40914  liminfvalxr  40923  fourierdlem31  41282  ovnval  41682  ovnval2  41686  ovnval2b  41693  ovolval2  41785  ovnovollem3  41799  smfinf  41951  smfinfmpt  41952  prmdvdsfmtnof1  42520