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

Theorem necon3bii 2653
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 2647 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2601 . 2  |-  ( C  =/=  D  <->  -.  C  =  D )
42, 3bitr4i 255 1  |-  ( A  =/=  B  <->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    = wceq 1437    =/= wne 2599
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 188  df-ne 2601
This theorem is referenced by:  necom  2654  neeq1i  2665  neeq2i  2666  neeq12i  2667  rnsnn0  5264  onoviun  7017  onnseq  7018  intrnfi  7883  wdomtr  8043  noinfep  8117  wemapwe  8154  scott0s  8311  cplem1  8312  karden  8318  acndom2  8436  dfac5lem3  8507  fin23lem31  8724  fin23lem40  8732  isf34lem5  8759  isf34lem7  8760  isf34lem6  8761  axrrecex  9538  negne0bi  9898  rpnnen1lem4  11244  rpnnen1lem5  11245  fseqsupcl  12140  limsupgre  13485  limsupgreOLD  13486  isercolllem3  13673  rpnnen2  14221  ruclem11  14235  3dvds  14312  prmreclem6  14808  0ram  14921  0ram2  14922  0ramcl  14924  gsumval2  16466  ghmrn  16839  gexex  17434  gsumval3  17484  iinopn  19874  cnconn  20379  1stcfb  20402  qtopeu  20673  fbasrn  20841  alexsublem  21001  evth  21929  minveclem1  22308  minveclem3b  22312  minveclem3bOLD  22324  ovollb2  22384  ovolunlem1a  22391  ovolunlem1  22392  ovoliunlem1  22397  ovoliun2  22401  ioombl1lem4  22456  uniioombllem1  22480  uniioombllem2  22482  uniioombllem2OLD  22483  uniioombllem6  22488  mbfsup  22562  mbfinf  22563  mbfinfOLD  22564  mbflimsup  22565  mbflimsupOLD  22566  itg1climres  22614  itg2monolem1  22650  itg2mono  22653  itg2i1fseq2  22656  sincos4thpi  23410  axlowdimlem13  24926  eupath  25651  siii  26436  minvecolem1  26458  bcsiALT  26774  h1de2bi  27149  h1de2ctlem  27150  nmlnopgt0i  27592  rge0scvg  28707  erdszelem5  29870  cvmsss2  29949  elrn3  30354  rankeq1o  30887  fin2so  31839  heicant  31882  scottn0f  32320  fnwe2lem2  35822  wnefimgd  36513
  Copyright terms: Public domain W3C validator