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

Theorem necon3bii 2725
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 2717 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2654 . 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 1395    =/= wne 2652
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 2654
This theorem is referenced by:  necom  2726  neeq1i  2742  neeq2i  2744  neeq12i  2746  rnsnn0  5480  onoviun  7032  onnseq  7033  intrnfi  7894  wdomtr  8019  noinfep  8093  noinfepOLD  8094  wemapwe  8156  wemapweOLD  8157  scott0s  8323  cplem1  8324  karden  8330  acndom2  8452  dfac5lem3  8523  fin23lem31  8740  fin23lem40  8748  isf34lem5  8775  isf34lem7  8776  isf34lem6  8777  axrrecex  9557  negne0bi  9911  rpnnen1lem4  11236  rpnnen1lem5  11237  fseqsupcl  12090  limsupgre  13316  isercolllem3  13501  rpnnen2  13971  ruclem11  13985  3dvds  14062  prmreclem6  14451  0ram  14550  0ram2  14551  0ramcl  14553  gsumval2  16034  ghmrn  16407  gexex  16986  gsumval3OLD  17035  gsumval3  17038  iinopn  19538  cnconn  20049  1stcfb  20072  qtopeu  20343  fbasrn  20511  alexsublem  20670  evth  21585  minveclem1  21965  minveclem3b  21969  ovollb2  22026  ovolunlem1a  22033  ovolunlem1  22034  ovoliunlem1  22039  ovoliun2  22043  ioombl1lem4  22097  uniioombllem1  22116  uniioombllem2  22118  uniioombllem6  22123  mbfsup  22197  mbfinf  22198  mbflimsup  22199  itg1climres  22247  itg2monolem1  22283  itg2mono  22286  itg2i1fseq2  22289  sincos4thpi  23032  axlowdimlem13  24384  eupath  25108  siii  25895  minvecolem1  25917  bcsiALT  26223  h1de2bi  26599  h1de2ctlem  26600  nmlnopgt0i  27043  rge0scvg  28092  erdszelem5  28836  cvmsss2  28916  elrn3  29410  rankeq1o  30033  fin2so  30245  heicant  30254  scottn0f  30783  fnwe2lem2  31201  wnefimgd  38166
  Copyright terms: Public domain W3C validator