Theorem neeq12i 3003

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypotheses

Ref	Expression
neeq1i.1	⊢ 𝐴 = 𝐵
neeq12i.2	⊢ 𝐶 = 𝐷

Assertion

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

Proof of Theorem neeq12i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
2		neeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
3	1, 2	eqeq12i 2746	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
4	3	necon3bii 2989	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Syntax hints:   ↔ wb 205   = wceq 1534   ≠ wne 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-ne 2937

This theorem is referenced by:  3netr3g  3015  3netr4g  3016  starvndxnbasendx  17278  starvndxnplusgndx  17279  starvndxnmulrndx  17280  scandxnbasendx  17290  scandxnplusgndx  17291  scandxnmulrndx  17292  vscandxnbasendx  17295  vscandxnplusgndx  17296  vscandxnmulrndx  17297  vscandxnscandx  17298  ipndxnbasendx  17306  ipndxnplusgndx  17307  ipndxnmulrndx  17308  slotsdifipndx  17309  tsetndxnplusgndx  17331  tsetndxnmulrndx  17332  tsetndxnstarvndx  17333  slotstnscsi  17334  plendxnplusgndx  17345  plendxnmulrndx  17346  plendxnscandx  17347  plendxnvscandx  17348  slotsdifplendx  17349  basendxnocndx  17357  plendxnocndx  17358  dsndxnplusgndx  17364  dsndxnmulrndx  17365  slotsdnscsi  17366  dsndxntsetndx  17367  slotsdifdsndx  17368  unifndxntsetndx  17374  slotsdifunifndx  17375  slotsdifplendx2  17391  slotsdifocndx  17392  oppchomfvalOLD  17688  oppcbasOLD  17693  rescbasOLD  17806  resccoOLD  17810  rescabsOLD  17812  odubasOLD  18277  oppglemOLD  19295  mgplemOLD  20072  mgpressOLD  20083  opprlemOLD  20272  sralemOLD  21055  srascaOLD  21063  sravscaOLD  21065  znbaslemOLD  21462  thlbasOLD  21622  thlleOLD  21624  opsrbaslemOLD  21981  matscaOLD  22309  tuslemOLD  24165  setsmsbasOLD  24375  setsmsdsOLD  24377  tngdsOLD  24558  nosepne  27606  lngndxnitvndx  28240  ttgvalOLD  28673  ttglemOLD  28675  cchhllemOLD  28691  axlowdimlem6  28751  zlmdsOLD  33558  zlmtsetOLD  33560  hlhilslemOLD  41406  oaomoencom  42740  zlmodzxzldeplem  47560  line2  47819  prstclevalOLD  48069  prstcocvalOLD  48072