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

Theorem necon3bii 2635
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 2633 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2603 . 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 1369    =/= wne 2601
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 2603
This theorem is referenced by:  necom  2688  rnsnn0  5300  onoviun  6796  onnseq  6797  intrnfi  7658  wdomtr  7782  noinfep  7857  noinfepOLD  7858  wemapwe  7920  wemapweOLD  7921  scott0s  8087  cplem1  8088  karden  8094  acndom2  8216  dfac5lem3  8287  fin23lem31  8504  fin23lem40  8512  isf34lem5  8539  isf34lem7  8540  isf34lem6  8541  axrrecex  9322  negne0bi  9673  rpnnen1lem4  10974  rpnnen1lem5  10975  fseqsupcl  11791  limsupgre  12951  isercolllem3  13136  rpnnen2  13500  ruclem11  13514  3dvds  13588  prmreclem6  13974  0ram  14073  0ram2  14074  0ramcl  14076  gsumval2  15504  ghmrn  15751  gexex  16326  gsumval3OLD  16373  gsumval3  16376  iinopn  18495  cnconn  19006  1stcfb  19029  qtopeu  19269  fbasrn  19437  alexsublem  19596  evth  20511  minveclem1  20891  minveclem3b  20895  ovollb2  20952  ovolunlem1a  20959  ovolunlem1  20960  ovoliunlem1  20965  ovoliun2  20969  ioombl1lem4  21022  uniioombllem1  21041  uniioombllem2  21043  uniioombllem6  21048  mbfsup  21122  mbfinf  21123  mbflimsup  21124  itg1climres  21172  itg2monolem1  21208  itg2mono  21211  itg2i1fseq2  21214  sincos4thpi  21955  axlowdimlem13  23168  eupath  23570  siii  24221  minvecolem1  24243  bcsiALT  24549  h1de2bi  24925  h1de2ctlem  24926  nmlnopgt0i  25369  rge0scvg  26348  erdszelem5  27052  cvmsss2  27132  elrn3  27542  rankeq1o  28178  fin2so  28387  heicant  28397  scottn0f  28953  fnwe2lem2  29375
  Copyright terms: Public domain W3C validator