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

Theorem necon3bii 2491
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 2489 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2461 . 2  |-  ( C  =/=  D  <->  -.  C  =  D )
42, 3bitr4i 243 1  |-  ( A  =/=  B  <->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necom  2540  rnsnn0  5155  onoviun  6376  onnseq  6377  intrnfi  7186  wdomtr  7305  noinfep  7376  noinfepOLD  7377  wemapwe  7416  scott0s  7574  cplem1  7575  karden  7581  acndom2  7697  dfac5lem3  7768  fin23lem31  7985  fin23lem40  7993  isf34lem5  8020  isf34lem7  8021  isf34lem6  8022  axrrecex  8801  negne0bi  9135  rpnnen1lem4  10361  rpnnen1lem5  10362  fseqsupcl  11055  limsupgre  11971  isercolllem3  12156  rpnnen2  12520  ruclem11  12534  3dvds  12607  prmreclem6  12984  0ram  13083  0ram2  13084  0ramcl  13086  gsumval2  14476  ghmrn  14712  gexex  15161  gsumval3  15207  iinopn  16664  cnconn  17164  1stcfb  17187  qtopeu  17423  fbasrn  17595  alexsublem  17754  evth  18473  minveclem1  18804  minveclem3b  18808  ovollb2  18864  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliun2  18881  ioombl1lem4  18934  uniioombllem1  18952  uniioombllem2  18954  uniioombllem6  18959  mbfsup  19035  mbfinf  19036  mbflimsup  19037  itg1climres  19085  itg2monolem1  19121  itg2mono  19124  itg2i1fseq2  19127  sincos4thpi  19897  siii  21447  minvecolem1  21469  bcsiALT  21774  h1de2bi  22149  h1de2ctlem  22150  nmlnopgt0i  22593  rge0scvg  23388  erdszelem5  23741  cvmsss2  23820  eupath  23920  elrn3  24191  axlowdimlem13  24654  rankeq1o  24873  fnwe2lem2  27251
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator