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

Theorem eqnetri 2763
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 2752 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 209 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  eqnetrri  2764  notzfaus  4628  2on0  7151  1n0  7157  noinfep  8088  card1  8361  fin23lem31  8735  tan0  13764  resslem  14565  xrsnsgrp  18324  matbas  18784  matplusg  18785  matvsca  18787  ustuqtop1  20612  iaa  22588  tan4thpi  22773  ang180lem2  23008  mcubic  23044  quart1lem  23052  resvlem  27646  esumnul  27884  ballotth  28301  bpoly4  29748  mncn0  31017  aaitgo  31040  stirlinglem11  31707  uhgrepe  32168  plusgndxnmulrndx  32353  basendxnmulrndx  32354  sec0  32636  2p2ne5  32695  bj-1upln0  34049  bj-2upln0  34063  bj-2upln1upl  34064
  Copyright terms: Public domain W3C validator