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 1542  wne 2940
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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  xpcoidgend  14866  fclsfnflim  23394  ptcmplem2  23420  vieta1lem1  25686  vieta1lem2  25687  fsuppcurry1  31689  fsuppcurry2  31690  signsvfpn  33254  signsvfnn  33255  finxpreclem2  35907  finxp1o  35909  cdleme3h  38744  cdleme7ga  38757  imo72b2lem1  42530  fourierdlem42  44476
  Copyright terms: Public domain W3C validator