Theorem infeq1d 9387

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

Syntax hints:   → wi 4   = wceq 1540  infcinf 9350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-ss 3922  df-uni 4862  df-sup 9351  df-inf 9352

This theorem is referenced by:  limsupval  15399  lcmval  16521  lcmass  16543  lcmfval  16550  lcmf0val  16551  lcmfpr  16556  odzval  16721  ramval  16938  imasval  17433  imasdsval  17437  gexval  19475  nmofval  24618  nmoval  24619  metdsval  24752  lebnumlem1  24876  lebnumlem3  24878  ovolval  25390  ovolshft  25428  ioorf  25490  mbflimsup  25583  ig1pval  26097  elqaalem1  26243  elqaalem2  26244  elqaalem3  26245  elqaa  26246  omsval  34263  omsfval  34264  ballotlemi  34471  pellfundval  42856  dgraaval  43120  supminfrnmpt  45428  infxrpnf  45429  infxrpnf2  45446  supminfxr  45447  supminfxr2  45452  supminfxrrnmpt  45454  limsupval3  45677  limsupresre  45681  limsupresico  45685  limsuppnfdlem  45686  limsupvaluz  45693  limsupvaluzmpt  45702  liminfval  45744  liminfgval  45747  liminfval5  45750  limsupresxr  45751  liminfresxr  45752  liminfval2  45753  liminfresico  45756  liminf10ex  45759  liminfvalxr  45768  fourierdlem31  46123  ovnval  46526  ovnval2  46530  ovnval2b  46537  ovolval2  46629  ovnovollem3  46643  smfinf  46803  smfinfmpt  46804  prmdvdsfmtnof1  47575