Theorem neeq12i 3007

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3netr3g  3019  3netr4g  3020  starvndxnbasendx  17348  starvndxnplusgndx  17349  starvndxnmulrndx  17350  scandxnbasendx  17360  scandxnplusgndx  17361  scandxnmulrndx  17362  vscandxnbasendx  17365  vscandxnplusgndx  17366  vscandxnmulrndx  17367  vscandxnscandx  17368  ipndxnbasendx  17376  ipndxnplusgndx  17377  ipndxnmulrndx  17378  slotsdifipndx  17379  tsetndxnplusgndx  17401  tsetndxnmulrndx  17402  tsetndxnstarvndx  17403  slotstnscsi  17404  plendxnplusgndx  17415  plendxnmulrndx  17416  plendxnscandx  17417  plendxnvscandx  17418  slotsdifplendx  17419  basendxnocndx  17427  plendxnocndx  17428  dsndxnplusgndx  17434  dsndxnmulrndx  17435  slotsdnscsi  17436  dsndxntsetndx  17437  slotsdifdsndx  17438  unifndxntsetndx  17444  slotsdifunifndx  17445  slotsdifplendx2  17461  slotsdifocndx  17462  rescabsOLD  17878  odubasOLD  18337  oppglemOLD  19369  opprlemOLD  20340  sralemOLD  21176  srascaOLD  21184  sravscaOLD  21186  znbaslemOLD  21554  thlbasOLD  21715  thlleOLD  21717  opsrbaslemOLD  22068  matscaOLD  22420  tuslemOLD  24276  setsmsbasOLD  24486  setsmsdsOLD  24488  tngdsOLD  24669  nosepne  27725  lngndxnitvndx  28451  ttgvalOLD  28884  ttglemOLD  28886  cchhllemOLD  28902  axlowdimlem6  28962  zlmdsOLD  33962  zlmtsetOLD  33964  hlhilslemOLD  41941  oaomoencom  43330  zlmodzxzldeplem  48415  line2  48673  prstclevalOLD  49158  prstcocvalOLD  49161