Theorem necon3bii 2993

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 2987	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷)
3		df-ne 2941	. 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
4	2, 3	bitr4i 278	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  necom  2994  neeq1i  3005  neeq2i  3006  neeq12i  3007  rnsnn0  6228  onoviun  8383  onnseq  8384  intrnfi  9456  wdomtr  9615  noinfep  9700  wemapwe  9737  scott0s  9928  cplem1  9929  karden  9935  acndom2  10094  dfac5lem3  10165  fin23lem31  10383  fin23lem40  10391  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  axrrecex  11203  negne0bi  11582  rpnnen1lem4  13022  rpnnen1lem5  13023  fseqsupcl  14018  limsupgre  15517  isercolllem3  15703  rpnnen2lem12  16261  ruclem11  16276  3dvds  16368  prmreclem6  16959  0ram  17058  0ram2  17059  0ramcl  17061  gsumval2  18699  ghmrn  19247  gexex  19871  gsumval3  19925  subdrgint  20804  iinopn  22908  cnconn  23430  1stcfb  23453  qtopeu  23724  fbasrn  23892  alexsublem  24052  evth  24991  minveclem1  25458  minveclem3b  25462  ovollb2  25524  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun2  25541  ioombl1lem4  25596  uniioombllem1  25616  uniioombllem2  25618  uniioombllem6  25623  mbfsup  25699  mbfinf  25700  mbflimsup  25701  itg1climres  25749  itg2monolem1  25785  itg2mono  25788  itg2i1fseq2  25791  sincos4thpi  26555  nosepnelem  27724  axlowdimlem13  28969  eulerpath  30260  siii  30872  minvecolem1  30893  bcsiALT  31198  h1de2bi  31573  h1de2ctlem  31574  nmlnopgt0i  32016  wrdpmtrlast  33113  dimval  33651  dimvalfi  33652  rge0scvg  33948  umgracycusgr  35159  cusgracyclt3v  35161  erdszelem5  35200  cvmsss2  35279  elrn3  35762  rankeq1o  36172  fin2so  37614  heicant  37662  scottn0f  38177  psspwb  42267  fnwe2lem2  43063  sqrtcval  43654