Theorem infeq1d 9388

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

Syntax hints:   → wi 4   = wceq 1547  infcinf 9351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-ss 3907  df-uni 4846  df-sup 9352  df-inf 9353

This theorem is referenced by:  limsupval  15434  lcmval  16559  lcmass  16581  lcmfval  16588  lcmf0val  16589  lcmfpr  16594  odzval  16760  ramval  16977  imasval  17473  imasdsval  17477  gexval  19551  nmofval  24704  nmoval  24705  metdsval  24838  lebnumlem1  24953  lebnumlem3  24955  ovolval  25465  ovolshft  25503  ioorf  25565  mbflimsup  25658  ig1pval  26166  elqaalem1  26310  elqaalem2  26311  elqaalem3  26312  elqaa  26313  omsval  34484  omsfval  34485  ballotlemi  34692  pellfundval  43332  dgraaval  43596  supminfrnmpt  45895  infxrpnf  45896  infxrpnf2  45913  supminfxr  45914  supminfxr2  45919  supminfxrrnmpt  45921  limsupval3  46142  limsupresre  46146  limsupresico  46150  limsuppnfdlem  46151  limsupvaluz  46158  limsupvaluzmpt  46167  liminfval  46209  liminfgval  46212  liminfval5  46215  limsupresxr  46216  liminfresxr  46217  liminfval2  46218  liminfresico  46221  liminf10ex  46224  liminfvalxr  46233  fourierdlem31  46588  ovnval  46991  ovnval2  46995  ovnval2b  47002  ovolval2  47094  ovnovollem3  47108  smfinf  47268  smfinfmpt  47269  prmdvdsfmtnof1  48072