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

Theorem necon3bii 2735
Description: Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
Hypothesis
Ref Expression
necon3bii.1  |-  ( A  =  B  <->  C  =  D )
Assertion
Ref Expression
necon3bii  |-  ( A  =/=  B  <->  C  =/=  D )

Proof of Theorem necon3bii
StepHypRef Expression
1 necon3bii.1 . . 3  |-  ( A  =  B  <->  C  =  D )
21necon3abii 2727 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2664 . 2  |-  ( C  =/=  D  <->  -.  C  =  D )
42, 3bitr4i 252 1  |-  ( A  =/=  B  <->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2664
This theorem is referenced by:  necom  2736  neeq1i  2752  neeq2i  2754  neeq12i  2756  rnsnn0  5480  onoviun  7026  onnseq  7027  intrnfi  7888  wdomtr  8013  noinfep  8088  noinfepOLD  8089  wemapwe  8151  wemapweOLD  8152  scott0s  8318  cplem1  8319  karden  8325  acndom2  8447  dfac5lem3  8518  fin23lem31  8735  fin23lem40  8743  isf34lem5  8770  isf34lem7  8771  isf34lem6  8772  axrrecex  9552  negne0bi  9904  rpnnen1lem4  11223  rpnnen1lem5  11224  fseqsupcl  12067  limsupgre  13284  isercolllem3  13469  rpnnen2  13837  ruclem11  13851  3dvds  13926  prmreclem6  14315  0ram  14414  0ram2  14415  0ramcl  14417  gsumval2  15781  ghmrn  16152  gexex  16732  gsumval3OLD  16781  gsumval3  16784  iinopn  19280  cnconn  19791  1stcfb  19814  qtopeu  20085  fbasrn  20253  alexsublem  20412  evth  21327  minveclem1  21707  minveclem3b  21711  ovollb2  21768  ovolunlem1a  21775  ovolunlem1  21776  ovoliunlem1  21781  ovoliun2  21785  ioombl1lem4  21839  uniioombllem1  21858  uniioombllem2  21860  uniioombllem6  21865  mbfsup  21939  mbfinf  21940  mbflimsup  21941  itg1climres  21989  itg2monolem1  22025  itg2mono  22028  itg2i1fseq2  22031  sincos4thpi  22772  axlowdimlem13  24080  eupath  24804  siii  25591  minvecolem1  25613  bcsiALT  25919  h1de2bi  26295  h1de2ctlem  26296  nmlnopgt0i  26739  rge0scvg  27756  erdszelem5  28464  cvmsss2  28544  elrn3  29119  rankeq1o  29755  fin2so  29967  heicant  29976  scottn0f  30506  fnwe2lem2  30925
  Copyright terms: Public domain W3C validator