Theorem neeq12i 2998

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

Syntax hints:   ↔ wb 206   = wceq 1540   ≠ wne 2932

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ne 2933

This theorem is referenced by:  3netr3g  3010  3netr4g  3011  starvndxnbasendx  17318  starvndxnplusgndx  17319  starvndxnmulrndx  17320  scandxnbasendx  17330  scandxnplusgndx  17331  scandxnmulrndx  17332  vscandxnbasendx  17335  vscandxnplusgndx  17336  vscandxnmulrndx  17337  vscandxnscandx  17338  ipndxnbasendx  17346  ipndxnplusgndx  17347  ipndxnmulrndx  17348  slotsdifipndx  17349  tsetndxnplusgndx  17371  tsetndxnmulrndx  17372  tsetndxnstarvndx  17373  slotstnscsi  17374  plendxnplusgndx  17385  plendxnmulrndx  17386  plendxnscandx  17387  plendxnvscandx  17388  slotsdifplendx  17389  basendxnocndx  17397  plendxnocndx  17398  dsndxnplusgndx  17404  dsndxnmulrndx  17405  slotsdnscsi  17406  dsndxntsetndx  17407  slotsdifdsndx  17408  unifndxntsetndx  17414  slotsdifunifndx  17415  slotsdifplendx2  17430  slotsdifocndx  17431  nosepne  27644  lngndxnitvndx  28422  axlowdimlem6  28926  oaomoencom  43341  gpgprismgr4cycllem7  48100  zlmodzxzldeplem  48474  line2  48732