Theorem neeq12i 2994

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

Syntax hints:   ↔ wb 206   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  3netr3g  3006  3netr4g  3007  starvndxnbasendx  17203  starvndxnplusgndx  17204  starvndxnmulrndx  17205  scandxnbasendx  17215  scandxnplusgndx  17216  scandxnmulrndx  17217  vscandxnbasendx  17220  vscandxnplusgndx  17221  vscandxnmulrndx  17222  vscandxnscandx  17223  ipndxnbasendx  17231  ipndxnplusgndx  17232  ipndxnmulrndx  17233  slotsdifipndx  17234  tsetndxnplusgndx  17256  tsetndxnmulrndx  17257  tsetndxnstarvndx  17258  slotstnscsi  17259  plendxnplusgndx  17270  plendxnmulrndx  17271  plendxnscandx  17272  plendxnvscandx  17273  slotsdifplendx  17274  basendxnocndx  17282  plendxnocndx  17283  dsndxnplusgndx  17289  dsndxnmulrndx  17290  slotsdnscsi  17291  dsndxntsetndx  17292  slotsdifdsndx  17293  unifndxntsetndx  17299  slotsdifunifndx  17300  slotsdifplendx2  17315  slotsdifocndx  17316  nosepne  27614  lngndxnitvndx  28416  axlowdimlem6  28920  oaomoencom  43350  gpgprismgr4cycllem7  48132  zlmodzxzldeplem  48530  line2  48784