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

Theorem eqnetri 2716
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 2705 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 212 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    =/= wne 2614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2616
This theorem is referenced by:  eqnetrri  2717  notzfaus  4599  2on0  7202  1n0  7208  noinfep  8173  card1  8410  fin23lem31  8780  bpoly4  14111  tan0  14204  resslem  15181  slotsbhcdif  15317  xrsnsgrp  19003  matbas  19436  matplusg  19437  matvsca  19439  ustuqtop1  21254  iaa  23279  tan4thpi  23467  ang180lem2  23737  mcubic  23771  quart1lem  23779  resvlem  28602  esumnul  28877  ballotth  29378  ballotthOLD  29416  quad3  30310  bj-1upln0  31571  bj-2upln0  31585  bj-2upln1upl  31586  mncn0  35968  aaitgo  35998  stirlinglem11  37886  plusgndxnmulrndx  39572  basendxnmulrndx  39573  sec0  40101  2p2ne5  40158
  Copyright terms: Public domain W3C validator