Theorem infeq1d 9495

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

Syntax hints:   → wi 4   = wceq 1540  infcinf 9458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-ss 3948  df-uni 4889  df-sup 9459  df-inf 9460

This theorem is referenced by:  limsupval  15495  lcmval  16616  lcmass  16638  lcmfval  16645  lcmf0val  16646  lcmfpr  16651  odzval  16816  ramval  17033  imasval  17530  imasdsval  17534  gexval  19564  nmofval  24658  nmoval  24659  metdsval  24792  lebnumlem1  24916  lebnumlem3  24918  ovolval  25431  ovolshft  25469  ioorf  25531  mbflimsup  25624  ig1pval  26138  elqaalem1  26284  elqaalem2  26285  elqaalem3  26286  elqaa  26287  omsval  34330  omsfval  34331  ballotlemi  34538  pellfundval  42870  dgraaval  43135  supminfrnmpt  45439  infxrpnf  45440  infxrpnf2  45457  supminfxr  45458  supminfxr2  45463  supminfxrrnmpt  45465  limsupval3  45688  limsupresre  45692  limsupresico  45696  limsuppnfdlem  45697  limsupvaluz  45704  limsupvaluzmpt  45713  liminfval  45755  liminfgval  45758  liminfval5  45761  limsupresxr  45762  liminfresxr  45763  liminfval2  45764  liminfresico  45767  liminf10ex  45770  liminfvalxr  45779  fourierdlem31  46134  ovnval  46537  ovnval2  46541  ovnval2b  46548  ovolval2  46640  ovnovollem3  46654  smfinf  46814  smfinfmpt  46815  prmdvdsfmtnof1  47568