MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqnetri Structured version   Unicode version

Theorem eqnetri 2748
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetr.1  |-  A  =  B
eqnetr.2  |-  B  =/= 
C
Assertion
Ref Expression
eqnetri  |-  A  =/= 
C

Proof of Theorem eqnetri
StepHypRef Expression
1 eqnetr.2 . 2  |-  B  =/= 
C
2 eqnetr.1 . . 3  |-  A  =  B
32neeq1i 2737 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 209 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    =/= wne 2648
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2650
This theorem is referenced by:  eqnetrri  2749  notzfaus  4578  2on0  7042  1n0  7048  noinfep  7980  card1  8253  fin23lem31  8627  tan0  13557  resslem  14354  matbas  18449  matplusg  18450  matvsca  18452  ustuqtop1  19958  iaa  21934  tan4thpi  22119  ang180lem2  22349  mcubic  22385  quart1lem  22393  resvlem  26467  esumnul  26670  ballotth  27087  bpoly4  28369  mncn0  29667  aaitgo  29690  stirlinglem11  30050  sec0  31446  2p2ne5  31505  bj-1upln0  32859  bj-2upln0  32873  bj-2upln1upl  32874
  Copyright terms: Public domain W3C validator