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

Theorem eqnetrrid 3027
 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 3020 1 (𝜑𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2952 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-ne 2953 This theorem is referenced by:  xpcoidgend  14383  fclsfnflim  22728  ptcmplem2  22754  vieta1lem1  25006  vieta1lem2  25007  fsuppcurry1  30585  fsuppcurry2  30586  signsvfpn  32084  signsvfnn  32085  finxpreclem2  35088  finxp1o  35090  cdleme3h  37812  cdleme7ga  37825  imo72b2lem1  41248  fourierdlem42  43158
 Copyright terms: Public domain W3C validator