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 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  3netr3g  3034  3netr4g  3035  starvndxnbasendx  17475  starvndxnplusgndx  17476  starvndxnmulrndx  17477  scandxnbasendx  17487  scandxnplusgndx  17488  scandxnmulrndx  17489  vscandxnbasendx  17492  vscandxnplusgndx  17493  vscandxnmulrndx  17494  vscandxnscandx  17495  ipndxnbasendx  17503  ipndxnplusgndx  17504  ipndxnmulrndx  17505  slotsdifipndx  17506  tsetndxnplusgndx  17528  tsetndxnmulrndx  17529  tsetndxnstarvndx  17530  slotstnscsi  17531  plendxnplusgndx  17542  plendxnmulrndx  17543  plendxnscandx  17544  plendxnvscandx  17545  slotsdifplendx  17546  basendxnocndx  17554  plendxnocndx  17555  dsndxnplusgndx  17561  dsndxnmulrndx  17562  slotsdnscsi  17563  dsndxntsetndx  17564  slotsdifdsndx  17565  unifndxntsetndx  17571  slotsdifunifndx  17572  slotsdifplendx2  17587  slotsdifocndx  17588  nosepne  28037  lngndxnitvndx  28905  axlowdimlem6  29525  oaomoencom  44318  gpgprismgr4cycllem7  49198  zlmodzxzldeplem  49609  line2  49863