Theorem neeq12i 2999

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

Syntax hints:   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  3netr3g  3011  3netr4g  3012  starvndxnbasendx  17258  starvndxnplusgndx  17259  starvndxnmulrndx  17260  scandxnbasendx  17270  scandxnplusgndx  17271  scandxnmulrndx  17272  vscandxnbasendx  17275  vscandxnplusgndx  17276  vscandxnmulrndx  17277  vscandxnscandx  17278  ipndxnbasendx  17286  ipndxnplusgndx  17287  ipndxnmulrndx  17288  slotsdifipndx  17289  tsetndxnplusgndx  17311  tsetndxnmulrndx  17312  tsetndxnstarvndx  17313  slotstnscsi  17314  plendxnplusgndx  17325  plendxnmulrndx  17326  plendxnscandx  17327  plendxnvscandx  17328  slotsdifplendx  17329  basendxnocndx  17337  plendxnocndx  17338  dsndxnplusgndx  17344  dsndxnmulrndx  17345  slotsdnscsi  17346  dsndxntsetndx  17347  slotsdifdsndx  17348  unifndxntsetndx  17354  slotsdifunifndx  17355  slotsdifplendx2  17370  slotsdifocndx  17371  nosepne  27658  lngndxnitvndx  28525  axlowdimlem6  29030  oaomoencom  43763  gpgprismgr4cycllem7  48589  zlmodzxzldeplem  48986  line2  49240