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 2600 . 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 1652    =/= wne 2598
This theorem is referenced by:  necom  2679  rnsnn0  5328  onoviun  6597  onnseq  6598  intrnfi  7413  wdomtr  7535  noinfep  7606  noinfepOLD  7607  wemapwe  7646  scott0s  7804  cplem1  7805  karden  7811  acndom2  7927  dfac5lem3  7998  fin23lem31  8215  fin23lem40  8223  isf34lem5  8250  isf34lem7  8251  isf34lem6  8252  axrrecex  9030  negne0bi  9365  rpnnen1lem4  10595  rpnnen1lem5  10596  fseqsupcl  11308  limsupgre  12267  isercolllem3  12452  rpnnen2  12817  ruclem11  12831  3dvds  12904  prmreclem6  13281  0ram  13380  0ram2  13381  0ramcl  13383  gsumval2  14775  ghmrn  15011  gexex  15460  gsumval3  15506  iinopn  16967  cnconn  17477  1stcfb  17500  qtopeu  17740  fbasrn  17908  alexsublem  18067  evth  18976  minveclem1  19317  minveclem3b  19321  ovollb2  19377  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliun2  19394  ioombl1lem4  19447  uniioombllem1  19465  uniioombllem2  19467  uniioombllem6  19472  mbfsup  19548  mbfinf  19549  mbflimsup  19550  itg1climres  19598  itg2monolem1  19634  itg2mono  19637  itg2i1fseq2  19640  sincos4thpi  20413  eupath  21695  siii  22346  minvecolem1  22368  bcsiALT  22673  h1de2bi  23048  h1de2ctlem  23049  nmlnopgt0i  23492  rge0scvg  24327  erdszelem5  24873  cvmsss2  24953  elrn3  25378  axlowdimlem13  25885  rankeq1o  26104  fnwe2lem2  27117
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 2600
  Copyright terms: Public domain W3C validator