Theorem neeq12i 3010

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 2756	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
4	3	necon3bii 2996	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Syntax hints:   ↔ wb 205   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  3netr3g  3022  3netr4g  3023  starvndxnbasendx  17014  starvndxnplusgndx  17015  starvndxnmulrndx  17016  scandxnbasendx  17026  scandxnplusgndx  17027  scandxnmulrndx  17028  vscandxnbasendx  17031  vscandxnplusgndx  17032  vscandxnmulrndx  17033  vscandxnscandx  17034  ipndxnbasendx  17042  ipndxnplusgndx  17043  ipndxnmulrndx  17044  slotsdifipndx  17045  tsetndxnplusgndx  17067  tsetndxnmulrndx  17068  tsetndxnstarvndx  17069  slotstnscsi  17070  plendxnplusgndx  17081  plendxnmulrndx  17082  plendxnscandx  17083  plendxnvscandx  17084  slotsdifplendx  17085  basendxnocndx  17093  plendxnocndx  17094  dsndxnplusgndx  17100  dsndxnmulrndx  17101  slotsdnscsi  17102  dsndxntsetndx  17103  slotsdifdsndx  17104  unifndxntsetndx  17110  slotsdifunifndx  17111  slotsdifplendx2  17127  slotsdifocndx  17128  oppchomfvalOLD  17424  oppcbasOLD  17429  rescbasOLD  17542  resccoOLD  17546  rescabsOLD  17548  odubasOLD  18010  oppglemOLD  18955  mgplemOLD  19725  mgpressOLD  19736  opprlemOLD  19868  sralemOLD  20440  srascaOLD  20448  sravscaOLD  20450  znbaslemOLD  20743  thlbasOLD  20902  thlleOLD  20904  opsrbaslemOLD  21251  matscaOLD  21563  tuslemOLD  23419  setsmsbasOLD  23629  setsmsdsOLD  23631  tngdsOLD  23812  lngndxnitvndx  26804  ttgvalOLD  27237  ttglemOLD  27239  cchhllemOLD  27255  axlowdimlem6  27315  zlmdsOLD  31913  zlmtsetOLD  31915  nosepne  33883  hlhilslemOLD  39953  zlmodzxzldeplem  45839  line2  46098  prstclevalOLD  46350  prstcocvalOLD  46353