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

Theorem necon3bii 2716
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 2708 . 2  |-  ( A  =/=  B  <->  -.  C  =  D )
3 df-ne 2646 . 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 1370    =/= wne 2644
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 2646
This theorem is referenced by:  necom  2717  neeq1i  2733  neeq2i  2735  neeq12i  2737  rnsnn0  5403  onoviun  6904  onnseq  6905  intrnfi  7767  wdomtr  7891  noinfep  7966  noinfepOLD  7967  wemapwe  8029  wemapweOLD  8030  scott0s  8196  cplem1  8197  karden  8203  acndom2  8325  dfac5lem3  8396  fin23lem31  8613  fin23lem40  8621  isf34lem5  8648  isf34lem7  8649  isf34lem6  8650  axrrecex  9431  negne0bi  9782  rpnnen1lem4  11083  rpnnen1lem5  11084  fseqsupcl  11900  limsupgre  13061  isercolllem3  13246  rpnnen2  13610  ruclem11  13624  3dvds  13698  prmreclem6  14084  0ram  14183  0ram2  14184  0ramcl  14186  gsumval2  15615  ghmrn  15862  gexex  16439  gsumval3OLD  16486  gsumval3  16489  iinopn  18631  cnconn  19142  1stcfb  19165  qtopeu  19405  fbasrn  19573  alexsublem  19732  evth  20647  minveclem1  21027  minveclem3b  21031  ovollb2  21088  ovolunlem1a  21095  ovolunlem1  21096  ovoliunlem1  21101  ovoliun2  21105  ioombl1lem4  21158  uniioombllem1  21177  uniioombllem2  21179  uniioombllem6  21184  mbfsup  21258  mbfinf  21259  mbflimsup  21260  itg1climres  21308  itg2monolem1  21344  itg2mono  21347  itg2i1fseq2  21350  sincos4thpi  22091  axlowdimlem13  23335  eupath  23737  siii  24388  minvecolem1  24410  bcsiALT  24716  h1de2bi  25092  h1de2ctlem  25093  nmlnopgt0i  25536  rge0scvg  26513  erdszelem5  27217  cvmsss2  27297  elrn3  27707  rankeq1o  28343  fin2so  28554  heicant  28564  scottn0f  29120  fnwe2lem2  29542
  Copyright terms: Public domain W3C validator