Theorem neeq12i 3013

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

Syntax hints:   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  3netr3g  3025  3netr4g  3026  starvndxnbasendx  17363  starvndxnplusgndx  17364  starvndxnmulrndx  17365  scandxnbasendx  17375  scandxnplusgndx  17376  scandxnmulrndx  17377  vscandxnbasendx  17380  vscandxnplusgndx  17381  vscandxnmulrndx  17382  vscandxnscandx  17383  ipndxnbasendx  17391  ipndxnplusgndx  17392  ipndxnmulrndx  17393  slotsdifipndx  17394  tsetndxnplusgndx  17416  tsetndxnmulrndx  17417  tsetndxnstarvndx  17418  slotstnscsi  17419  plendxnplusgndx  17430  plendxnmulrndx  17431  plendxnscandx  17432  plendxnvscandx  17433  slotsdifplendx  17434  basendxnocndx  17442  plendxnocndx  17443  dsndxnplusgndx  17449  dsndxnmulrndx  17450  slotsdnscsi  17451  dsndxntsetndx  17452  slotsdifdsndx  17453  unifndxntsetndx  17459  slotsdifunifndx  17460  slotsdifplendx2  17476  slotsdifocndx  17477  oppchomfvalOLD  17773  oppcbasOLD  17778  rescbasOLD  17891  resccoOLD  17895  rescabsOLD  17897  odubasOLD  18362  oppglemOLD  19391  mgplemOLD  20166  mgpressOLD  20177  opprlemOLD  20366  sralemOLD  21199  srascaOLD  21207  sravscaOLD  21209  znbaslemOLD  21577  thlbasOLD  21738  thlleOLD  21740  opsrbaslemOLD  22091  matscaOLD  22441  tuslemOLD  24297  setsmsbasOLD  24507  setsmsdsOLD  24509  tngdsOLD  24690  nosepne  27743  lngndxnitvndx  28469  ttgvalOLD  28902  ttglemOLD  28904  cchhllemOLD  28920  axlowdimlem6  28980  zlmdsOLD  33909  zlmtsetOLD  33911  hlhilslemOLD  41896  oaomoencom  43279  zlmodzxzldeplem  48227  line2  48486  prstclevalOLD  48736  prstcocvalOLD  48739