Theorem infeq1d 8266

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

Syntax hints:   → wi 4   = wceq 1475  infcinf 8230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-uni 4373  df-sup 8231  df-inf 8232

This theorem is referenced by:  limsupval  14053  lcmval  15143  lcmass  15165  lcmfval  15172  lcmf0val  15173  lcmfpr  15178  odzval  15334  ramval  15550  imasval  15994  imasdsval  15998  gexval  17816  nmofval  22328  nmoval  22329  metdsval  22458  lebnumlem1  22568  lebnumlem3  22570  ovolval  23049  ovolshft  23086  ioorf  23147  mbflimsup  23239  ig1pval  23736  elqaalem1  23878  elqaalem2  23879  elqaalem3  23880  elqaa  23881  omsval  29682  omsfval  29683  ballotlemi  29889  pellfundval  36462  dgraaval  36733  fourierdlem31  39031  ovnval  39431  ovnval2  39435  ovnval2b  39442  ovolval2  39534  ovnovollem3  39548  prmdvdsfmtnof1  40037