Theorem necon3bii 2984

Description: Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)

Hypothesis

Ref	Expression
necon3bii.1	⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)

Assertion

Ref	Expression
necon3bii	⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)

Proof of Theorem necon3bii

Step	Hyp	Ref	Expression
1		necon3bii.1	. . 3 ⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)
2	1	necon3abii 2978	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷)
3		df-ne 2933	. 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
4	2, 3	bitr4i 278	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  necom  2985  neeq1i  2996  neeq2i  2997  neeq12i  2998  rnsnn0  6166  onoviun  8275  onnseq  8276  intrnfi  9319  wdomtr  9480  noinfep  9569  wemapwe  9606  scott0s  9800  cplem1  9801  karden  9807  acndom2  9964  dfac5lem3  10035  fin23lem31  10253  fin23lem40  10261  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  axrrecex  11074  negne0bi  11454  rpnnen1lem4  12893  rpnnen1lem5  12894  fseqsupcl  13900  limsupgre  15404  isercolllem3  15590  rpnnen2lem12  16150  ruclem11  16165  3dvds  16258  prmreclem6  16849  0ram  16948  0ram2  16949  0ramcl  16951  gsumval2  18611  ghmrn  19158  gexex  19782  gsumval3  19836  subdrgint  20736  iinopn  22846  cnconn  23366  1stcfb  23389  qtopeu  23660  fbasrn  23828  alexsublem  23988  evth  24914  minveclem1  25380  minveclem3b  25384  ovollb2  25446  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliun2  25463  ioombl1lem4  25518  uniioombllem1  25538  uniioombllem2  25540  uniioombllem6  25545  mbfsup  25621  mbfinf  25622  mbflimsup  25623  itg1climres  25671  itg2monolem1  25707  itg2mono  25710  itg2i1fseq2  25713  sincos4thpi  26478  nosepnelem  27647  axlowdimlem13  29027  eulerpath  30316  siii  30928  minvecolem1  30949  bcsiALT  31254  h1de2bi  31629  h1de2ctlem  31630  nmlnopgt0i  32072  wrdpmtrlast  33175  dimval  33757  dimvalfi  33758  rge0scvg  34106  umgracycusgr  35348  cusgracyclt3v  35350  erdszelem5  35389  cvmsss2  35468  elrn3  35956  rankeq1o  36365  regsfromunir1  36670  fin2so  37808  heicant  37856  scottn0f  38371  psspwb  42484  fnwe2lem2  43293  sqrtcval  43882