Theorem neeq12i 2995

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

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

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 2123  ax-ext 2705

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

This theorem is referenced by:  3netr3g  3007  3netr4g  3008  starvndxnbasendx  17215  starvndxnplusgndx  17216  starvndxnmulrndx  17217  scandxnbasendx  17227  scandxnplusgndx  17228  scandxnmulrndx  17229  vscandxnbasendx  17232  vscandxnplusgndx  17233  vscandxnmulrndx  17234  vscandxnscandx  17235  ipndxnbasendx  17243  ipndxnplusgndx  17244  ipndxnmulrndx  17245  slotsdifipndx  17246  tsetndxnplusgndx  17268  tsetndxnmulrndx  17269  tsetndxnstarvndx  17270  slotstnscsi  17271  plendxnplusgndx  17282  plendxnmulrndx  17283  plendxnscandx  17284  plendxnvscandx  17285  slotsdifplendx  17286  basendxnocndx  17294  plendxnocndx  17295  dsndxnplusgndx  17301  dsndxnmulrndx  17302  slotsdnscsi  17303  dsndxntsetndx  17304  slotsdifdsndx  17305  unifndxntsetndx  17311  slotsdifunifndx  17312  slotsdifplendx2  17327  slotsdifocndx  17328  nosepne  27639  lngndxnitvndx  28441  axlowdimlem6  28946  oaomoencom  43474  gpgprismgr4cycllem7  48263  zlmodzxzldeplem  48660  line2  48914