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

Theorem eqnetrrid 3017
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 3010 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wne 2941
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 2942
This theorem is referenced by:  xpcoidgend  14922  fclsfnflim  23531  ptcmplem2  23557  vieta1lem1  25823  vieta1lem2  25824  fsuppcurry1  31950  fsuppcurry2  31951  signsvfpn  33596  signsvfnn  33597  finxpreclem2  36271  finxp1o  36273  cdleme3h  39106  cdleme7ga  39119  imo72b2lem1  42921  fourierdlem42  44865
  Copyright terms: Public domain W3C validator