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

Theorem eqnetri 2615
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 2608 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 201 1  |-  A  =/= 
C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    =/= wne 2598
This theorem is referenced by:  eqnetrri  2617  notzfaus  4366  2on0  6725  1n0  6731  noinfep  7606  card1  7847  fin23lem31  8215  tan0  12744  resslem  13514  ustuqtop1  18263  iaa  20234  tan4thpi  20414  ang180lem2  20644  mcubic  20679  quart1lem  20687  esumnul  24435  ballotth  24787  bpoly4  26097  mncn0  27312  aaitgo  27335  matbas  27436  matplusg  27437  matvsca  27439  stirlinglem11  27800  sec0  28440  2p2ne5  28473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428  df-ne 2600
  Copyright terms: Public domain W3C validator