Theorem neeq12i 3022

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

Syntax hints:   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  3netr3g  3034  3netr4g  3035  starvndxnbasendx  17324  starvndxnplusgndx  17325  starvndxnmulrndx  17326  scandxnbasendx  17336  scandxnplusgndx  17337  scandxnmulrndx  17338  vscandxnbasendx  17341  vscandxnplusgndx  17342  vscandxnmulrndx  17343  vscandxnscandx  17344  ipndxnbasendx  17352  ipndxnplusgndx  17353  ipndxnmulrndx  17354  slotsdifipndx  17355  tsetndxnplusgndx  17377  tsetndxnmulrndx  17378  tsetndxnstarvndx  17379  slotstnscsi  17380  plendxnplusgndx  17391  plendxnmulrndx  17392  plendxnscandx  17393  plendxnvscandx  17394  slotsdifplendx  17395  basendxnocndx  17403  plendxnocndx  17404  dsndxnplusgndx  17410  dsndxnmulrndx  17411  slotsdnscsi  17412  dsndxntsetndx  17413  slotsdifdsndx  17414  unifndxntsetndx  17420  slotsdifunifndx  17421  slotsdifplendx2  17436  slotsdifocndx  17437  nosepne  27732  lngndxnitvndx  28600  axlowdimlem6  29105  oaomoencom  43855  gpgprismgr4cycllem7  48684  zlmodzxzldeplem  49081  line2  49335