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

Theorem necon3bii 2478
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 2476 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  necom  2527  rnsnn0  5139  onoviun  6360  onnseq  6361  intrnfi  7170  wdomtr  7289  noinfep  7360  noinfepOLD  7361  wemapwe  7400  scott0s  7558  cplem1  7559  karden  7565  acndom2  7681  dfac5lem3  7752  fin23lem31  7969  fin23lem40  7977  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  axrrecex  8785  negne0bi  9119  rpnnen1lem4  10345  rpnnen1lem5  10346  fseqsupcl  11039  limsupgre  11955  isercolllem3  12140  rpnnen2  12504  ruclem11  12518  3dvds  12591  prmreclem6  12968  0ram  13067  0ram2  13068  0ramcl  13070  gsumval2  14460  ghmrn  14696  gexex  15145  gsumval3  15191  iinopn  16648  cnconn  17148  1stcfb  17171  qtopeu  17407  fbasrn  17579  alexsublem  17738  evth  18457  minveclem1  18788  minveclem3b  18792  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliun2  18865  ioombl1lem4  18918  uniioombllem1  18936  uniioombllem2  18938  uniioombllem6  18943  mbfsup  19019  mbfinf  19020  mbflimsup  19021  itg1climres  19069  itg2monolem1  19105  itg2mono  19108  itg2i1fseq2  19111  sincos4thpi  19881  siii  21431  minvecolem1  21453  bcsiALT  21758  h1de2bi  22133  h1de2ctlem  22134  nmlnopgt0i  22577  rge0scvg  23373  erdszelem5  23726  cvmsss2  23805  eupath  23905  elrn3  24120  axlowdimlem13  24582  rankeq1o  24801  fnwe2lem2  27148
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 2448
  Copyright terms: Public domain W3C validator