Theorem neeq12i 3025

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3netr3g  3037  3netr4g  3038  suppvalbr  8218  starvndxnbasendx  17521  starvndxnplusgndx  17522  starvndxnmulrndx  17523  scandxnbasendx  17533  scandxnplusgndx  17534  scandxnmulrndx  17535  vscandxnbasendx  17538  vscandxnplusgndx  17539  vscandxnmulrndx  17540  vscandxnscandx  17541  ipndxnbasendx  17549  ipndxnplusgndx  17550  ipndxnmulrndx  17551  slotsdifipndx  17552  tsetndxnplusgndx  17574  tsetndxnmulrndx  17575  tsetndxnstarvndx  17576  slotstnscsi  17577  plendxnplusgndx  17588  plendxnmulrndx  17589  plendxnscandx  17590  plendxnvscandx  17591  slotsdifplendx  17592  basendxnocndx  17600  plendxnocndx  17601  dsndxnplusgndx  17607  dsndxnmulrndx  17608  slotsdnscsi  17609  dsndxntsetndx  17610  slotsdifdsndx  17611  unifndxntsetndx  17617  slotsdifunifndx  17618  slotsdifplendx2  17637  slotsdifocndx  17638  nosepne  28094  lngndxnitvndx  28962  axlowdimlem6  29582  oaomoencom  44580  gpgprismgr4cycllem7  49472  zlmodzxzldeplem  49941  line2  50195