Theorem necon3bii 2980

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

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

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 2929

This theorem is referenced by:  necom  2981  neeq1i  2992  neeq2i  2993  neeq12i  2994  rnsnn0  6155  onoviun  8263  onnseq  8264  intrnfi  9300  wdomtr  9461  noinfep  9550  wemapwe  9587  scott0s  9781  cplem1  9782  karden  9788  acndom2  9945  dfac5lem3  10016  fin23lem31  10234  fin23lem40  10242  isf34lem5  10269  isf34lem7  10270  isf34lem6  10271  axrrecex  11054  negne0bi  11434  rpnnen1lem4  12878  rpnnen1lem5  12879  fseqsupcl  13884  limsupgre  15388  isercolllem3  15574  rpnnen2lem12  16134  ruclem11  16149  3dvds  16242  prmreclem6  16833  0ram  16932  0ram2  16933  0ramcl  16935  gsumval2  18594  ghmrn  19142  gexex  19766  gsumval3  19820  subdrgint  20719  iinopn  22818  cnconn  23338  1stcfb  23361  qtopeu  23632  fbasrn  23800  alexsublem  23960  evth  24886  minveclem1  25352  minveclem3b  25356  ovollb2  25418  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliun2  25435  ioombl1lem4  25490  uniioombllem1  25510  uniioombllem2  25512  uniioombllem6  25517  mbfsup  25593  mbfinf  25594  mbflimsup  25595  itg1climres  25643  itg2monolem1  25679  itg2mono  25682  itg2i1fseq2  25685  sincos4thpi  26450  nosepnelem  27619  axlowdimlem13  28933  eulerpath  30219  siii  30831  minvecolem1  30852  bcsiALT  31157  h1de2bi  31532  h1de2ctlem  31533  nmlnopgt0i  31975  wrdpmtrlast  33060  dimval  33611  dimvalfi  33612  rge0scvg  33960  umgracycusgr  35196  cusgracyclt3v  35198  erdszelem5  35237  cvmsss2  35316  elrn3  35804  rankeq1o  36211  fin2so  37653  heicant  37701  scottn0f  38216  psspwb  42267  fnwe2lem2  43090  sqrtcval  43680