Theorem neeq12i 3005

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  3netr3g  3017  3netr4g  3018  starvndxnbasendx  17253  starvndxnplusgndx  17254  starvndxnmulrndx  17255  scandxnbasendx  17265  scandxnplusgndx  17266  scandxnmulrndx  17267  vscandxnbasendx  17270  vscandxnplusgndx  17271  vscandxnmulrndx  17272  vscandxnscandx  17273  ipndxnbasendx  17281  ipndxnplusgndx  17282  ipndxnmulrndx  17283  slotsdifipndx  17284  tsetndxnplusgndx  17306  tsetndxnmulrndx  17307  tsetndxnstarvndx  17308  slotstnscsi  17309  plendxnplusgndx  17320  plendxnmulrndx  17321  plendxnscandx  17322  plendxnvscandx  17323  slotsdifplendx  17324  basendxnocndx  17332  plendxnocndx  17333  dsndxnplusgndx  17339  dsndxnmulrndx  17340  slotsdnscsi  17341  dsndxntsetndx  17342  slotsdifdsndx  17343  unifndxntsetndx  17349  slotsdifunifndx  17350  slotsdifplendx2  17366  slotsdifocndx  17367  oppchomfvalOLD  17663  oppcbasOLD  17668  rescbasOLD  17781  resccoOLD  17785  rescabsOLD  17787  odubasOLD  18249  oppglemOLD  19256  mgplemOLD  20033  mgpressOLD  20044  opprlemOLD  20231  sralemOLD  20936  srascaOLD  20944  sravscaOLD  20946  znbaslemOLD  21310  thlbasOLD  21469  thlleOLD  21471  opsrbaslemOLD  21824  matscaOLD  22136  tuslemOLD  23992  setsmsbasOLD  24202  setsmsdsOLD  24204  tngdsOLD  24385  nosepne  27419  lngndxnitvndx  27961  ttgvalOLD  28394  ttglemOLD  28396  cchhllemOLD  28412  axlowdimlem6  28472  zlmdsOLD  33241  zlmtsetOLD  33243  hlhilslemOLD  41113  oaomoencom  42369  zlmodzxzldeplem  47266  line2  47525  prstclevalOLD  47776  prstcocvalOLD  47779