Theorem neeq12i 2999

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

Syntax hints:   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  3netr3g  3011  3netr4g  3012  starvndxnbasendx  17236  starvndxnplusgndx  17237  starvndxnmulrndx  17238  scandxnbasendx  17248  scandxnplusgndx  17249  scandxnmulrndx  17250  vscandxnbasendx  17253  vscandxnplusgndx  17254  vscandxnmulrndx  17255  vscandxnscandx  17256  ipndxnbasendx  17264  ipndxnplusgndx  17265  ipndxnmulrndx  17266  slotsdifipndx  17267  tsetndxnplusgndx  17289  tsetndxnmulrndx  17290  tsetndxnstarvndx  17291  slotstnscsi  17292  plendxnplusgndx  17303  plendxnmulrndx  17304  plendxnscandx  17305  plendxnvscandx  17306  slotsdifplendx  17307  basendxnocndx  17315  plendxnocndx  17316  dsndxnplusgndx  17322  dsndxnmulrndx  17323  slotsdnscsi  17324  dsndxntsetndx  17325  slotsdifdsndx  17326  unifndxntsetndx  17332  slotsdifunifndx  17333  slotsdifplendx2  17348  slotsdifocndx  17349  nosepne  27660  lngndxnitvndx  28527  axlowdimlem6  29032  oaomoencom  43674  gpgprismgr4cycllem7  48461  zlmodzxzldeplem  48858  line2  49112