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 1570   ≠ wne 2955

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 2732

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

This theorem is used by:  3netr3g  3033  3netr4g  3034  starvndxnbasendx  17390  starvndxnplusgndx  17391  starvndxnmulrndx  17392  scandxnbasendx  17402  scandxnplusgndx  17403  scandxnmulrndx  17404  vscandxnbasendx  17407  vscandxnplusgndx  17408  vscandxnmulrndx  17409  vscandxnscandx  17410  ipndxnbasendx  17418  ipndxnplusgndx  17419  ipndxnmulrndx  17420  slotsdifipndx  17421  tsetndxnplusgndx  17443  tsetndxnmulrndx  17444  tsetndxnstarvndx  17445  slotstnscsi  17446  plendxnplusgndx  17457  plendxnmulrndx  17458  plendxnscandx  17459  plendxnvscandx  17460  slotsdifplendx  17461  basendxnocndx  17469  plendxnocndx  17470  dsndxnplusgndx  17476  dsndxnmulrndx  17477  slotsdnscsi  17478  dsndxntsetndx  17479  slotsdifdsndx  17480  unifndxntsetndx  17486  slotsdifunifndx  17487  slotsdifplendx2  17502  slotsdifocndx  17503  nosepne  27917  lngndxnitvndx  28785  axlowdimlem6  29405  oaomoencom  44159  gpgprismgr4cycllem7  49018  zlmodzxzldeplem  49429  line2  49683