Theorem neeq12i 2991

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3netr3g  3003  3netr4g  3004  starvndxnbasendx  17267  starvndxnplusgndx  17268  starvndxnmulrndx  17269  scandxnbasendx  17279  scandxnplusgndx  17280  scandxnmulrndx  17281  vscandxnbasendx  17284  vscandxnplusgndx  17285  vscandxnmulrndx  17286  vscandxnscandx  17287  ipndxnbasendx  17295  ipndxnplusgndx  17296  ipndxnmulrndx  17297  slotsdifipndx  17298  tsetndxnplusgndx  17320  tsetndxnmulrndx  17321  tsetndxnstarvndx  17322  slotstnscsi  17323  plendxnplusgndx  17334  plendxnmulrndx  17335  plendxnscandx  17336  plendxnvscandx  17337  slotsdifplendx  17338  basendxnocndx  17346  plendxnocndx  17347  dsndxnplusgndx  17353  dsndxnmulrndx  17354  slotsdnscsi  17355  dsndxntsetndx  17356  slotsdifdsndx  17357  unifndxntsetndx  17363  slotsdifunifndx  17364  slotsdifplendx2  17379  slotsdifocndx  17380  nosepne  27592  lngndxnitvndx  28370  axlowdimlem6  28874  oaomoencom  43306  gpgprismgr4cycllem7  48091  zlmodzxzldeplem  48487  line2  48741