Theorem neeq12i 3008

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

Syntax hints:   ↔ wb 205   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  3netr3g  3020  3netr4g  3021  starvndxnbasendx  17249  starvndxnplusgndx  17250  starvndxnmulrndx  17251  scandxnbasendx  17261  scandxnplusgndx  17262  scandxnmulrndx  17263  vscandxnbasendx  17266  vscandxnplusgndx  17267  vscandxnmulrndx  17268  vscandxnscandx  17269  ipndxnbasendx  17277  ipndxnplusgndx  17278  ipndxnmulrndx  17279  slotsdifipndx  17280  tsetndxnplusgndx  17302  tsetndxnmulrndx  17303  tsetndxnstarvndx  17304  slotstnscsi  17305  plendxnplusgndx  17316  plendxnmulrndx  17317  plendxnscandx  17318  plendxnvscandx  17319  slotsdifplendx  17320  basendxnocndx  17328  plendxnocndx  17329  dsndxnplusgndx  17335  dsndxnmulrndx  17336  slotsdnscsi  17337  dsndxntsetndx  17338  slotsdifdsndx  17339  unifndxntsetndx  17345  slotsdifunifndx  17346  slotsdifplendx2  17362  slotsdifocndx  17363  oppchomfvalOLD  17659  oppcbasOLD  17664  rescbasOLD  17777  resccoOLD  17781  rescabsOLD  17783  odubasOLD  18245  oppglemOLD  19215  mgplemOLD  19992  mgpressOLD  20003  opprlemOLD  20156  sralemOLD  20791  srascaOLD  20799  sravscaOLD  20801  znbaslemOLD  21091  thlbasOLD  21250  thlleOLD  21252  opsrbaslemOLD  21605  matscaOLD  21916  tuslemOLD  23772  setsmsbasOLD  23982  setsmsdsOLD  23984  tngdsOLD  24165  nosepne  27183  lngndxnitvndx  27694  ttgvalOLD  28127  ttglemOLD  28129  cchhllemOLD  28145  axlowdimlem6  28205  zlmdsOLD  32943  zlmtsetOLD  32945  hlhilslemOLD  40810  oaomoencom  42067  zlmodzxzldeplem  47179  line2  47438  prstclevalOLD  47689  prstcocvalOLD  47692