Theorem infeq1d 9467

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

Syntax hints:   → wi 4   = wceq 1533  infcinf 9431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-in 3947  df-ss 3957  df-uni 4900  df-sup 9432  df-inf 9433

This theorem is referenced by:  limsupval  15414  lcmval  16525  lcmass  16547  lcmfval  16554  lcmf0val  16555  lcmfpr  16560  odzval  16722  ramval  16939  imasval  17455  imasdsval  17459  gexval  19487  nmofval  24552  nmoval  24553  metdsval  24684  lebnumlem1  24808  lebnumlem3  24810  ovolval  25323  ovolshft  25361  ioorf  25423  mbflimsup  25516  ig1pval  26029  elqaalem1  26172  elqaalem2  26173  elqaalem3  26174  elqaa  26175  omsval  33747  omsfval  33748  ballotlemi  33954  pellfundval  42073  dgraaval  42341  supminfrnmpt  44606  infxrpnf  44607  infxrpnf2  44624  supminfxr  44625  supminfxr2  44630  supminfxrrnmpt  44632  limsupval3  44859  limsupresre  44863  limsupresico  44867  limsuppnfdlem  44868  limsupvaluz  44875  limsupvaluzmpt  44884  liminfval  44926  liminfgval  44929  liminfval5  44932  limsupresxr  44933  liminfresxr  44934  liminfval2  44935  liminfresico  44938  liminf10ex  44941  liminfvalxr  44950  fourierdlem31  45305  ovnval  45708  ovnval2  45712  ovnval2b  45719  ovolval2  45811  ovnovollem3  45825  smfinf  45985  smfinfmpt  45986  prmdvdsfmtnof1  46706