Theorem necon3bii 2991

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  necom  2992  neeq1i  3003  neeq2i  3004  neeq12i  3005  rnsnn0  6206  onoviun  8345  onnseq  8346  intrnfi  9413  wdomtr  9572  noinfep  9657  wemapwe  9694  scott0s  9885  cplem1  9886  karden  9892  acndom2  10051  dfac5lem3  10122  fin23lem31  10340  fin23lem40  10348  isf34lem5  10375  isf34lem7  10376  isf34lem6  10377  axrrecex  11160  negne0bi  11537  rpnnen1lem4  12968  rpnnen1lem5  12969  fseqsupcl  13946  limsupgre  15429  isercolllem3  15617  rpnnen2lem12  16172  ruclem11  16187  3dvds  16278  prmreclem6  16858  0ram  16957  0ram2  16958  0ramcl  16960  gsumval2  18611  ghmrn  19143  gexex  19762  gsumval3  19816  subdrgint  20562  iinopn  22624  cnconn  23146  1stcfb  23169  qtopeu  23440  fbasrn  23608  alexsublem  23768  evth  24705  minveclem1  25172  minveclem3b  25176  ovollb2  25238  ovolunlem1a  25245  ovolunlem1  25246  ovoliunlem1  25251  ovoliun2  25255  ioombl1lem4  25310  uniioombllem1  25330  uniioombllem2  25332  uniioombllem6  25337  mbfsup  25413  mbfinf  25414  mbflimsup  25415  itg1climres  25464  itg2monolem1  25500  itg2mono  25503  itg2i1fseq2  25506  sincos4thpi  26259  nosepnelem  27418  axlowdimlem13  28479  eulerpath  29761  siii  30373  minvecolem1  30394  bcsiALT  30699  h1de2bi  31074  h1de2ctlem  31075  nmlnopgt0i  31517  dimval  32973  dimvalfi  32974  rge0scvg  33227  umgracycusgr  34443  cusgracyclt3v  34445  erdszelem5  34484  cvmsss2  34563  elrn3  35036  rankeq1o  35447  fin2so  36778  heicant  36826  scottn0f  37341  psspwb  41352  fnwe2lem2  42095  sqrtcval  42694