Theorem neeq12i 3024

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 3010	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Syntax hints:   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  3netr3g  3036  3netr4g  3037  starvndxnbasendx  17352  starvndxnplusgndx  17353  starvndxnmulrndx  17354  scandxnbasendx  17364  scandxnplusgndx  17365  scandxnmulrndx  17366  vscandxnbasendx  17369  vscandxnplusgndx  17370  vscandxnmulrndx  17371  vscandxnscandx  17372  ipndxnbasendx  17380  ipndxnplusgndx  17381  ipndxnmulrndx  17382  slotsdifipndx  17383  tsetndxnplusgndx  17405  tsetndxnmulrndx  17406  tsetndxnstarvndx  17407  slotstnscsi  17408  plendxnplusgndx  17419  plendxnmulrndx  17420  plendxnscandx  17421  plendxnvscandx  17422  slotsdifplendx  17423  basendxnocndx  17431  plendxnocndx  17432  dsndxnplusgndx  17438  dsndxnmulrndx  17439  slotsdnscsi  17440  dsndxntsetndx  17441  slotsdifdsndx  17442  unifndxntsetndx  17448  slotsdifunifndx  17449  slotsdifplendx2  17464  slotsdifocndx  17465  nosepne  27844  lngndxnitvndx  28712  axlowdimlem6  29297  oaomoencom  44044  gpgprismgr4cycllem7  48866  zlmodzxzldeplem  49278  line2  49532