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

Theorem eqnetri 2694
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 2688 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 214 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1448    =/= wne 2622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-cleq 2445  df-ne 2624
This theorem is referenced by:  eqnetrri  2695  notzfaus  4551  2on0  7178  1n0  7184  noinfep  8152  card1  8389  fin23lem31  8760  bpoly4  14123  tan0  14216  resslem  15193  slotsbhcdif  15329  xrsnsgrp  19015  matbas  19449  matplusg  19450  matvsca  19452  ustuqtop1  21267  iaa  23293  tan4thpi  23481  ang180lem2  23751  mcubic  23785  quart1lem  23793  resvlem  28601  esumnul  28876  ballotth  29376  ballotthOLD  29414  quad3  30308  bj-1upln0  31605  bj-2upln0  31619  bj-2upln1upl  31620  mncn0  36000  aaitgo  36030  stirlinglem11  38003  plusgndxnmulrndx  40278  basendxnmulrndx  40279  sec0  40805  2p2ne5  40862
  Copyright terms: Public domain W3C validator