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

Theorem eqnetrrid 3016
Description: A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Hypotheses
Ref Expression
eqnetrrid.1 𝐵 = 𝐴
eqnetrrid.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqnetrrid (𝜑𝐴𝐶)

Proof of Theorem eqnetrrid
StepHypRef Expression
1 eqnetrrid.1 . . 3 𝐵 = 𝐴
21a1i 11 . 2 (𝜑𝐵 = 𝐴)
3 eqnetrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqnetrrd 3009 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941
This theorem is referenced by:  xpcoidgend  14924  fclsfnflim  23538  ptcmplem2  23564  vieta1lem1  25830  vieta1lem2  25831  fsuppcurry1  31988  fsuppcurry2  31989  signsvfpn  33665  signsvfnn  33666  finxpreclem2  36357  finxp1o  36359  cdleme3h  39192  cdleme7ga  39205  imo72b2lem1  43003  fourierdlem42  44944
  Copyright terms: Public domain W3C validator