Theorem neeq12i 2991

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

Syntax hints:   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  3netr3g  3003  3netr4g  3004  starvndxnbasendx  17227  starvndxnplusgndx  17228  starvndxnmulrndx  17229  scandxnbasendx  17239  scandxnplusgndx  17240  scandxnmulrndx  17241  vscandxnbasendx  17244  vscandxnplusgndx  17245  vscandxnmulrndx  17246  vscandxnscandx  17247  ipndxnbasendx  17255  ipndxnplusgndx  17256  ipndxnmulrndx  17257  slotsdifipndx  17258  tsetndxnplusgndx  17280  tsetndxnmulrndx  17281  tsetndxnstarvndx  17282  slotstnscsi  17283  plendxnplusgndx  17294  plendxnmulrndx  17295  plendxnscandx  17296  plendxnvscandx  17297  slotsdifplendx  17298  basendxnocndx  17306  plendxnocndx  17307  dsndxnplusgndx  17313  dsndxnmulrndx  17314  slotsdnscsi  17315  dsndxntsetndx  17316  slotsdifdsndx  17317  unifndxntsetndx  17323  slotsdifunifndx  17324  slotsdifplendx2  17339  slotsdifocndx  17340  nosepne  27609  lngndxnitvndx  28407  axlowdimlem6  28911  oaomoencom  43310  gpgprismgr4cycllem7  48105  zlmodzxzldeplem  48503  line2  48757