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

Theorem eqnetrrid 3015
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 3008 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wne 2939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ne 2940
This theorem is referenced by:  xpcoidgend  15015  fclsfnflim  24036  ptcmplem2  24062  vieta1lem1  26353  vieta1lem2  26354  fsuppcurry1  32737  fsuppcurry2  32738  signsvfpn  34601  signsvfnn  34602  finxpreclem2  37392  finxp1o  37394  cdleme3h  40238  cdleme7ga  40251  imo72b2lem0  44183  imo72b2lem1  44187  fourierdlem42  46169
  Copyright terms: Public domain W3C validator