Theorem infeq1d 9417

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

Syntax hints:   → wi 4   = wceq 1559  infcinf 9380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-ss 3919  df-uni 4863  df-sup 9381  df-inf 9382

This theorem is referenced by:  limsupval  15491  lcmval  16616  lcmass  16638  lcmfval  16645  lcmf0val  16646  lcmfpr  16651  odzval  16817  ramval  17034  imasval  17531  imasdsval  17535  gexval  19608  nmofval  24761  nmoval  24762  metdsval  24895  lebnumlem1  25010  lebnumlem3  25012  ovolval  25522  ovolshft  25560  ioorf  25622  mbflimsup  25715  ig1pval  26223  elqaalem1  26370  elqaalem2  26371  elqaalem3  26372  elqaa  26373  omsval  34550  omsfval  34551  ballotlemi  34758  pellfundval  43417  dgraaval  43681  supminfrnmpt  45979  infxrpnf  45980  infxrpnf2  45997  supminfxr  45998  supminfxr2  46003  supminfxrrnmpt  46005  limsupval3  46226  limsupresre  46230  limsupresico  46234  limsuppnfdlem  46235  limsupvaluz  46242  limsupvaluzmpt  46251  liminfval  46293  liminfgval  46296  liminfval5  46299  limsupresxr  46300  liminfresxr  46301  liminfval2  46302  liminfresico  46305  liminf10ex  46308  liminfvalxr  46317  fourierdlem31  46672  ovnval  47075  ovnval2  47079  ovnval2b  47086  ovolval2  47178  ovnovollem3  47192  smfinf  47352  smfinfmpt  47353  prmdvdsfmtnof1  48156