Theorem neeq12i 3005

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ne 2939

This theorem is referenced by:  3netr3g  3017  3netr4g  3018  starvndxnbasendx  17350  starvndxnplusgndx  17351  starvndxnmulrndx  17352  scandxnbasendx  17362  scandxnplusgndx  17363  scandxnmulrndx  17364  vscandxnbasendx  17367  vscandxnplusgndx  17368  vscandxnmulrndx  17369  vscandxnscandx  17370  ipndxnbasendx  17378  ipndxnplusgndx  17379  ipndxnmulrndx  17380  slotsdifipndx  17381  tsetndxnplusgndx  17403  tsetndxnmulrndx  17404  tsetndxnstarvndx  17405  slotstnscsi  17406  plendxnplusgndx  17417  plendxnmulrndx  17418  plendxnscandx  17419  plendxnvscandx  17420  slotsdifplendx  17421  basendxnocndx  17429  plendxnocndx  17430  dsndxnplusgndx  17436  dsndxnmulrndx  17437  slotsdnscsi  17438  dsndxntsetndx  17439  slotsdifdsndx  17440  unifndxntsetndx  17446  slotsdifunifndx  17447  slotsdifplendx2  17463  slotsdifocndx  17464  oppchomfvalOLD  17760  oppcbasOLD  17765  rescbasOLD  17878  resccoOLD  17882  rescabsOLD  17884  odubasOLD  18349  oppglemOLD  19382  mgplemOLD  20157  mgpressOLD  20168  opprlemOLD  20357  sralemOLD  21194  srascaOLD  21202  sravscaOLD  21204  znbaslemOLD  21572  thlbasOLD  21733  thlleOLD  21735  opsrbaslemOLD  22086  matscaOLD  22436  tuslemOLD  24292  setsmsbasOLD  24502  setsmsdsOLD  24504  tngdsOLD  24685  nosepne  27740  lngndxnitvndx  28466  ttgvalOLD  28899  ttglemOLD  28901  cchhllemOLD  28917  axlowdimlem6  28977  zlmdsOLD  33924  zlmtsetOLD  33926  hlhilslemOLD  41922  oaomoencom  43307  zlmodzxzldeplem  48344  line2  48602  prstclevalOLD  48870  prstcocvalOLD  48873