Theorem infeq1d 9474

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  infcinf 9437

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-uni 4867  df-sup 9438  df-inf 9439

This theorem is used by:  limsupval  15647  lcmval  16773  lcmass  16795  lcmfval  16802  lcmf0val  16803  lcmfpr  16808  odzval  16975  ramval  17192  imasval  17689  imasdsval  17693  gexval  19798  nmofval  25039  nmoval  25040  metdsval  25173  lebnumlem1  25288  lebnumlem3  25290  ovolval  25800  ovolshft  25838  ioorf  25900  mbflimsup  25993  ig1pval  26500  elqaalem1  26648  elqaalem2  26649  elqaalem3  26650  elqaa  26651  omsval  34972  omsfval  34973  ballotlemi  35180  frlmnzcoordval  43747  frlmnzcoordsca  43752  pellfundval  43981  dgraaval  44240  supminfrnmpt  46549  infxrpnf  46550  infxrpnf2  46567  supminfxr  46568  supminfxr2  46573  supminfxrrnmpt  46575  limsupval3  46796  limsupresre  46800  limsupresico  46804  limsuppnfdlem  46805  limsupvaluz  46812  limsupvaluzmpt  46821  liminfval  46863  liminfgval  46866  liminfval5  46869  limsupresxr  46870  liminfresxr  46871  liminfval2  46872  liminfresico  46875  liminf10ex  46878  liminfvalxr  46887  fourierdlem31  47242  ovnval  47645  ovnval2  47649  ovnval2b  47656  ovolval2  47748  ovnovollem3  47762  smfinf  47922  smfinfmpt  47923  prmdvdsfmtnof1  48766