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  17243  starvndxnplusgndx  17244  starvndxnmulrndx  17245  scandxnbasendx  17255  scandxnplusgndx  17256  scandxnmulrndx  17257  vscandxnbasendx  17260  vscandxnplusgndx  17261  vscandxnmulrndx  17262  vscandxnscandx  17263  ipndxnbasendx  17271  ipndxnplusgndx  17272  ipndxnmulrndx  17273  slotsdifipndx  17274  tsetndxnplusgndx  17296  tsetndxnmulrndx  17297  tsetndxnstarvndx  17298  slotstnscsi  17299  plendxnplusgndx  17310  plendxnmulrndx  17311  plendxnscandx  17312  plendxnvscandx  17313  slotsdifplendx  17314  basendxnocndx  17322  plendxnocndx  17323  dsndxnplusgndx  17329  dsndxnmulrndx  17330  slotsdnscsi  17331  dsndxntsetndx  17332  slotsdifdsndx  17333  unifndxntsetndx  17339  slotsdifunifndx  17340  slotsdifplendx2  17355  slotsdifocndx  17356  nosepne  27568  lngndxnitvndx  28346  axlowdimlem6  28850  oaomoencom  43279  gpgprismgr4cycllem7  48064  zlmodzxzldeplem  48460  line2  48714