Theorem neeq12i 3021

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  3netr3g  3033  3netr4g  3034  suppvalbr  8188  starvndxnbasendx  17484  starvndxnplusgndx  17485  starvndxnmulrndx  17486  scandxnbasendx  17496  scandxnplusgndx  17497  scandxnmulrndx  17498  vscandxnbasendx  17501  vscandxnplusgndx  17502  vscandxnmulrndx  17503  vscandxnscandx  17504  ipndxnbasendx  17512  ipndxnplusgndx  17513  ipndxnmulrndx  17514  slotsdifipndx  17515  tsetndxnplusgndx  17537  tsetndxnmulrndx  17538  tsetndxnstarvndx  17539  slotstnscsi  17540  plendxnplusgndx  17551  plendxnmulrndx  17552  plendxnscandx  17553  plendxnvscandx  17554  slotsdifplendx  17555  basendxnocndx  17563  plendxnocndx  17564  dsndxnplusgndx  17570  dsndxnmulrndx  17571  slotsdnscsi  17572  dsndxntsetndx  17573  slotsdifdsndx  17574  unifndxntsetndx  17580  slotsdifunifndx  17581  slotsdifplendx2  17596  slotsdifocndx  17597  nosepne  28046  lngndxnitvndx  28914  axlowdimlem6  29534  oaomoencom  44456  gpgprismgr4cycllem7  49335  zlmodzxzldeplem  49746  line2  50000