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

Theorem necon3bii 2599
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 2597 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2569 . 2  |-  ( C  =/=  D  <->  -.  C  =  D )
42, 3bitr4i 244 1  |-  ( A  =/=  B  <->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    = wceq 1649    =/= wne 2567
This theorem is referenced by:  necom  2648  rnsnn0  5295  onoviun  6564  onnseq  6565  intrnfi  7379  wdomtr  7499  noinfep  7570  noinfepOLD  7571  wemapwe  7610  scott0s  7768  cplem1  7769  karden  7775  acndom2  7891  dfac5lem3  7962  fin23lem31  8179  fin23lem40  8187  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  axrrecex  8994  negne0bi  9329  rpnnen1lem4  10559  rpnnen1lem5  10560  fseqsupcl  11271  limsupgre  12230  isercolllem3  12415  rpnnen2  12780  ruclem11  12794  3dvds  12867  prmreclem6  13244  0ram  13343  0ram2  13344  0ramcl  13346  gsumval2  14738  ghmrn  14974  gexex  15423  gsumval3  15469  iinopn  16930  cnconn  17438  1stcfb  17461  qtopeu  17701  fbasrn  17869  alexsublem  18028  evth  18937  minveclem1  19278  minveclem3b  19282  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliun2  19355  ioombl1lem4  19408  uniioombllem1  19426  uniioombllem2  19428  uniioombllem6  19433  mbfsup  19509  mbfinf  19510  mbflimsup  19511  itg1climres  19559  itg2monolem1  19595  itg2mono  19598  itg2i1fseq2  19601  sincos4thpi  20374  eupath  21656  siii  22307  minvecolem1  22329  bcsiALT  22634  h1de2bi  23009  h1de2ctlem  23010  nmlnopgt0i  23453  rge0scvg  24288  erdszelem5  24834  cvmsss2  24914  elrn3  25334  axlowdimlem13  25797  rankeq1o  26016  fnwe2lem2  27016
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2569
  Copyright terms: Public domain W3C validator