Theorem infeq1d 9381

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

Syntax hints:   → wi 4   = wceq 1541  infcinf 9344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-ss 3918  df-uni 4864  df-sup 9345  df-inf 9346

This theorem is referenced by:  limsupval  15397  lcmval  16519  lcmass  16541  lcmfval  16548  lcmf0val  16549  lcmfpr  16554  odzval  16719  ramval  16936  imasval  17432  imasdsval  17436  gexval  19507  nmofval  24658  nmoval  24659  metdsval  24792  lebnumlem1  24916  lebnumlem3  24918  ovolval  25430  ovolshft  25468  ioorf  25530  mbflimsup  25623  ig1pval  26137  elqaalem1  26283  elqaalem2  26284  elqaalem3  26285  elqaa  26286  omsval  34450  omsfval  34451  ballotlemi  34658  pellfundval  43122  dgraaval  43386  supminfrnmpt  45689  infxrpnf  45690  infxrpnf2  45707  supminfxr  45708  supminfxr2  45713  supminfxrrnmpt  45715  limsupval3  45936  limsupresre  45940  limsupresico  45944  limsuppnfdlem  45945  limsupvaluz  45952  limsupvaluzmpt  45961  liminfval  46003  liminfgval  46006  liminfval5  46009  limsupresxr  46010  liminfresxr  46011  liminfval2  46012  liminfresico  46015  liminf10ex  46018  liminfvalxr  46027  fourierdlem31  46382  ovnval  46785  ovnval2  46789  ovnval2b  46796  ovolval2  46888  ovnovollem3  46902  smfinf  47062  smfinfmpt  47063  prmdvdsfmtnof1  47833