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

Theorem necon3bii 2630
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 2628 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2598 . 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 1362    =/= wne 2596
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 2598
This theorem is referenced by:  necom  2683  rnsnn0  5293  onoviun  6790  onnseq  6791  intrnfi  7654  wdomtr  7778  noinfep  7853  noinfepOLD  7854  wemapwe  7916  wemapweOLD  7917  scott0s  8083  cplem1  8084  karden  8090  acndom2  8212  dfac5lem3  8283  fin23lem31  8500  fin23lem40  8508  isf34lem5  8535  isf34lem7  8536  isf34lem6  8537  axrrecex  9318  negne0bi  9669  rpnnen1lem4  10970  rpnnen1lem5  10971  fseqsupcl  11783  limsupgre  12943  isercolllem3  13128  rpnnen2  13491  ruclem11  13505  3dvds  13579  prmreclem6  13965  0ram  14064  0ram2  14065  0ramcl  14067  gsumval2  15493  ghmrn  15740  gexex  16315  gsumval3OLD  16362  gsumval3  16365  iinopn  18357  cnconn  18868  1stcfb  18891  qtopeu  19131  fbasrn  19299  alexsublem  19458  evth  20373  minveclem1  20753  minveclem3b  20757  ovollb2  20814  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliun2  20831  ioombl1lem4  20884  uniioombllem1  20903  uniioombllem2  20905  uniioombllem6  20910  mbfsup  20984  mbfinf  20985  mbflimsup  20986  itg1climres  21034  itg2monolem1  21070  itg2mono  21073  itg2i1fseq2  21076  sincos4thpi  21860  axlowdimlem13  23023  eupath  23425  siii  24076  minvecolem1  24098  bcsiALT  24404  h1de2bi  24780  h1de2ctlem  24781  nmlnopgt0i  25224  rge0scvg  26233  erdszelem5  26931  cvmsss2  27011  elrn3  27420  rankeq1o  28056  fin2so  28260  heicant  28270  scottn0f  28827  fnwe2lem2  29249
  Copyright terms: Public domain W3C validator