MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  infeq1d Structured version   Visualization version   GIF version

Theorem infeq1d 8335
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
StepHypRef Expression
1 infeq1d.1 . 2 (𝜑𝐵 = 𝐶)
2 infeq1 8334 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2syl 17 1 (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  infcinf 8299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-uni 4408  df-sup 8300  df-inf 8301
This theorem is referenced by:  limsupval  14147  lcmval  15240  lcmass  15262  lcmfval  15269  lcmf0val  15270  lcmfpr  15275  odzval  15431  ramval  15647  imasval  16103  imasdsval  16107  gexval  17925  nmofval  22441  nmoval  22442  metdsval  22573  lebnumlem1  22683  lebnumlem3  22685  ovolval  23165  ovolshft  23202  ioorf  23264  mbflimsup  23356  ig1pval  23853  elqaalem1  23995  elqaalem2  23996  elqaalem3  23997  elqaa  23998  omsval  30160  omsfval  30161  ballotlemi  30367  pellfundval  36959  dgraaval  37230  limsupval3  39356  limsupresre  39360  limsupresico  39364  limsuppnfdlem  39365  limsupvaluz  39372  limsupvaluzmpt  39381  fourierdlem31  39688  ovnval  40088  ovnval2  40092  ovnval2b  40099  ovolval2  40191  ovnovollem3  40205  smfinf  40357  smfinfmpt  40358  prmdvdsfmtnof1  40824
  Copyright terms: Public domain W3C validator