Theorem neeq12i 3000

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

Syntax hints:   ↔ wb 207   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  3netr3g  3012  3netr4g  3013  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  27662  lngndxnitvndx  28529  axlowdimlem6  29034  oaomoencom  43762  gpgprismgr4cycllem7  48592  zlmodzxzldeplem  48989  line2  49243