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

Theorem infeq1i 8267
 Description: Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
Hypothesis
Ref Expression
infeq1i.1 𝐵 = 𝐶
Assertion
Ref Expression
infeq1i inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)

Proof of Theorem infeq1i
StepHypRef Expression
1 infeq1i.1 . 2 𝐵 = 𝐶
2 infeq1 8265 . 2 (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
 Colors of variables: wff setvar class Syntax hints:   = 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:  infsn  8293  nninf  11645  nn0inf  11646  lcmcom  15144  lcmass  15165  lcmf0  15185  imasdsval2  15999  imasdsf1olem  21988  ftalem6  24604  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  elaa2  39127  etransc  39176  ioorrnopn  39201  ovnval2  39435  ovolval3  39537  vonioolem2  39572
 Copyright terms: Public domain W3C validator