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

Theorem necon3bii 2688
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 2682 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2635 . 2  |-  ( C  =/=  D  <->  -.  C  =  D )
42, 3bitr4i 260 1  |-  ( A  =/=  B  <->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189    = wceq 1455    =/= wne 2633
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 190  df-ne 2635
This theorem is referenced by:  necom  2689  neeq1i  2700  neeq2i  2701  neeq12i  2702  rnsnn0  5321  onoviun  7088  onnseq  7089  intrnfi  7956  wdomtr  8116  noinfep  8191  wemapwe  8228  scott0s  8385  cplem1  8386  karden  8392  acndom2  8511  dfac5lem3  8582  fin23lem31  8799  fin23lem40  8807  isf34lem5  8834  isf34lem7  8835  isf34lem6  8836  axrrecex  9613  negne0bi  9973  rpnnen1lem4  11322  rpnnen1lem5  11323  fseqsupcl  12222  limsupgre  13591  limsupgreOLD  13592  isercolllem3  13779  rpnnen2  14327  ruclem11  14341  3dvds  14418  prmreclem6  14914  0ram  15027  0ram2  15028  0ramcl  15030  gsumval2  16572  ghmrn  16945  gexex  17540  gsumval3  17590  iinopn  19981  cnconn  20486  1stcfb  20509  qtopeu  20780  fbasrn  20948  alexsublem  21108  evth  22036  minveclem1  22415  minveclem3b  22419  minveclem3bOLD  22431  ovollb2  22491  ovolunlem1a  22498  ovolunlem1  22499  ovoliunlem1  22504  ovoliun2  22508  ioombl1lem4  22563  uniioombllem1  22587  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem6  22595  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  mbflimsup  22672  mbflimsupOLD  22673  itg1climres  22721  itg2monolem1  22757  itg2mono  22760  itg2i1fseq2  22763  sincos4thpi  23517  axlowdimlem13  25033  eupath  25758  siii  26543  minvecolem1  26565  bcsiALT  26881  h1de2bi  27256  h1de2ctlem  27257  nmlnopgt0i  27699  rge0scvg  28804  erdszelem5  29967  cvmsss2  30046  elrn3  30452  rankeq1o  30987  fin2so  31977  heicant  32020  scottn0f  32458  fnwe2lem2  35954  wnefimgd  36645
  Copyright terms: Public domain W3C validator