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

Theorem eqnetri 2727
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 2716 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 212 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    =/= wne 2625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421  df-ne 2627
This theorem is referenced by:  eqnetrri  2728  notzfaus  4600  2on0  7199  1n0  7205  noinfep  8164  card1  8401  fin23lem31  8771  bpoly4  14090  tan0  14183  resslem  15144  slotsbhcdif  15277  xrsnsgrp  18939  matbas  19369  matplusg  19370  matvsca  19372  ustuqtop1  21187  iaa  23146  tan4thpi  23334  ang180lem2  23604  mcubic  23638  quart1lem  23646  resvlem  28433  esumnul  28708  ballotth  29196  quad3  30090  bj-1upln0  31352  bj-2upln0  31366  bj-2upln1upl  31367  mncn0  35703  aaitgo  35726  stirlinglem11  37514  uhgrepe  38447  plusgndxnmulrndx  38710  basendxnmulrndx  38711  sec0  39240  2p2ne5  39297
  Copyright terms: Public domain W3C validator