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

Theorem necon3bii 2582
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 2580 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2552 . 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 2550
This theorem is referenced by:  necom  2631  rnsnn0  5276  onoviun  6541  onnseq  6542  intrnfi  7356  wdomtr  7476  noinfep  7547  noinfepOLD  7548  wemapwe  7587  scott0s  7745  cplem1  7746  karden  7752  acndom2  7868  dfac5lem3  7939  fin23lem31  8156  fin23lem40  8164  isf34lem5  8191  isf34lem7  8192  isf34lem6  8193  axrrecex  8971  negne0bi  9305  rpnnen1lem4  10535  rpnnen1lem5  10536  fseqsupcl  11243  limsupgre  12202  isercolllem3  12387  rpnnen2  12752  ruclem11  12766  3dvds  12839  prmreclem6  13216  0ram  13315  0ram2  13316  0ramcl  13318  gsumval2  14710  ghmrn  14946  gexex  15395  gsumval3  15441  iinopn  16898  cnconn  17406  1stcfb  17429  qtopeu  17669  fbasrn  17837  alexsublem  17996  evth  18855  minveclem1  19192  minveclem3b  19196  ovollb2  19252  ovolunlem1a  19259  ovolunlem1  19260  ovoliunlem1  19265  ovoliun2  19269  ioombl1lem4  19322  uniioombllem1  19340  uniioombllem2  19342  uniioombllem6  19347  mbfsup  19423  mbfinf  19424  mbflimsup  19425  itg1climres  19473  itg2monolem1  19509  itg2mono  19512  itg2i1fseq2  19515  sincos4thpi  20288  eupath  21551  siii  22202  minvecolem1  22224  bcsiALT  22529  h1de2bi  22904  h1de2ctlem  22905  nmlnopgt0i  23348  rge0scvg  24139  erdszelem5  24660  cvmsss2  24740  elrn3  25144  axlowdimlem13  25607  rankeq1o  25826  fnwe2lem2  26817
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 2552
  Copyright terms: Public domain W3C validator