Theorem necon3bii 2846

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

Step	Hyp	Ref	Expression
1		necon3bii.1	. . 3 |- ( A = B <-> C = D )
2	1	necon3abii 2840	. 2 |- ( A =/= B <-> -. C = D )
3		df-ne 2795	. 2 |- ( C =/= D <-> -. C = D )
4	2, 3	bitr4i 267	1 |- ( A =/= B <-> C =/= D )

Syntax hints:   -. wn 3   <-> wb 196   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necom  2847  neeq1i  2858  neeq2i  2859  neeq12i  2860  rnsnn0  5601  onoviun  7440  onnseq  7441  intrnfi  8322  wdomtr  8480  noinfep  8557  wemapwe  8594  scott0s  8751  cplem1  8752  karden  8758  acndom2  8877  dfac5lem3  8948  fin23lem31  9165  fin23lem40  9173  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  axrrecex  9984  negne0bi  10354  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  fseqsupcl  12776  limsupgre  14212  isercolllem3  14397  rpnnen2lem12  14954  ruclem11  14969  3dvds  15052  3dvdsOLD  15053  prmreclem6  15625  0ram  15724  0ram2  15725  0ramcl  15727  gsumval2  17280  ghmrn  17673  gexex  18256  gsumval3  18308  iinopn  20707  cnconn  21225  1stcfb  21248  qtopeu  21519  fbasrn  21688  alexsublem  21848  evth  22758  minveclem1  23195  minveclem3b  23199  ovollb2  23257  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliun2  23274  ioombl1lem4  23329  uniioombllem1  23349  uniioombllem2  23351  uniioombllem6  23356  mbfsup  23431  mbfinf  23432  mbflimsup  23433  itg1climres  23481  itg2monolem1  23517  itg2mono  23520  itg2i1fseq2  23523  sincos4thpi  24265  axlowdimlem13  25834  eulerpath  27101  siii  27708  minvecolem1  27730  bcsiALT  28036  h1de2bi  28413  h1de2ctlem  28414  nmlnopgt0i  28856  rge0scvg  29995  erdszelem5  31177  cvmsss2  31256  elrn3  31652  nosepnelem  31830  rankeq1o  32278  fin2so  33396  heicant  33444  scottn0f  33978  fnwe2lem2  37621  wnefimgd  38460