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

Theorem eqnetri 2753
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 2742 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 209 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    =/= wne 2652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
This theorem is referenced by:  eqnetrri  2754  notzfaus  4631  2on0  7157  1n0  7163  noinfep  8093  card1  8366  fin23lem31  8740  tan0  13898  resslem  14704  slotsbhcdif  14837  xrsnsgrp  18581  matbas  19042  matplusg  19043  matvsca  19045  ustuqtop1  20870  iaa  22847  tan4thpi  23033  ang180lem2  23268  mcubic  23304  quart1lem  23312  resvlem  27982  esumnul  28222  ballotth  28673  quad3  29221  bpoly4  30026  mncn0  31292  aaitgo  31315  stirlinglem11  32069  uhgrepe  32640  plusgndxnmulrndx  32903  basendxnmulrndx  32904  sec0  33298  2p2ne5  33357  bj-1upln0  34710  bj-2upln0  34724  bj-2upln1upl  34725
  Copyright terms: Public domain W3C validator