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  19141  gexex  19765  gsumval3  19819  subdrgint  20718  iinopn  22817  cnconn  23337  1stcfb  23360  qtopeu  23631  fbasrn  23799  alexsublem  23959  evth  24885  minveclem1  25351  minveclem3b  25355  ovollb2  25417  ovolunlem1a  25424  ovolunlem1  25425  ovoliunlem1  25430  ovoliun2  25434  ioombl1lem4  25489  uniioombllem1  25509  uniioombllem2  25511  uniioombllem6  25516  mbfsup  25592  mbfinf  25593  mbflimsup  25594  itg1climres  25642  itg2monolem1  25678  itg2mono  25681  itg2i1fseq2  25684  sincos4thpi  26449  nosepnelem  27618  axlowdimlem13  28932  eulerpath  30221  siii  30833  minvecolem1  30854  bcsiALT  31159  h1de2bi  31534  h1de2ctlem  31535  nmlnopgt0i  31977  wrdpmtrlast  33062  dimval  33613  dimvalfi  33614  rge0scvg  33962  umgracycusgr  35198  cusgracyclt3v  35200  erdszelem5  35239  cvmsss2  35318  elrn3  35806  rankeq1o  36215  fin2so  37646  heicant  37694  scottn0f  38209  psspwb  42320  fnwe2lem2  43143  sqrtcval  43733