Theorem neeq12i 3030

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

Syntax hints:   ↔ wb 209   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  3netr3g  3042  3netr4g  3043  starvndxnbasendx  17353  starvndxnplusgndx  17354  starvndxnmulrndx  17355  scandxnbasendx  17365  scandxnplusgndx  17366  scandxnmulrndx  17367  vscandxnbasendx  17370  vscandxnplusgndx  17371  vscandxnmulrndx  17372  vscandxnscandx  17373  ipndxnbasendx  17381  ipndxnplusgndx  17382  ipndxnmulrndx  17383  slotsdifipndx  17384  tsetndxnplusgndx  17406  tsetndxnmulrndx  17407  tsetndxnstarvndx  17408  slotstnscsi  17409  plendxnplusgndx  17420  plendxnmulrndx  17421  plendxnscandx  17422  plendxnvscandx  17423  slotsdifplendx  17424  basendxnocndx  17432  plendxnocndx  17433  dsndxnplusgndx  17439  dsndxnmulrndx  17440  slotsdnscsi  17441  dsndxntsetndx  17442  slotsdifdsndx  17443  unifndxntsetndx  17449  slotsdifunifndx  17450  slotsdifplendx2  17465  slotsdifocndx  17466  nosepne  27806  lngndxnitvndx  28674  axlowdimlem6  29234  oaomoencom  43931  gpgprismgr4cycllem7  48750  zlmodzxzldeplem  49158  line2  49412