Theorem neeq12i 3009

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

Syntax hints:   ↔ wb 205   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  3netr3g  3021  3netr4g  3022  starvndxnbasendx  16940  starvndxnplusgndx  16941  starvndxnmulrndx  16942  scandxnbasendx  16952  scandxnplusgndx  16953  scandxnmulrndx  16954  vscandxnbasendx  16957  vscandxnplusgndx  16958  vscandxnmulrndx  16959  vscandxnscandx  16960  ipndxnbasendx  16968  ipndxnplusgndx  16969  ipndxnmulrndx  16970  tsetndxnplusgndx  16992  tsetndxnmulrndx  16993  slotstnscsi  16994  plendxnplusgndx  17005  plendxnmulrndx  17006  plendxnscandx  17007  plendxnvscandx  17008  dsndxnplusgndx  17021  dsndxnmulrndx  17022  slotsdnscsi  17023  dsndxntsetndx  17024  unifndxntsetndx  17030  oppchomfvalOLD  17341  oppcbasOLD  17346  rescbasOLD  17459  resccoOLD  17463  rescabs  17464  odubas  17925  oppglemOLD  18870  mgplemOLD  19640  mgpressOLD  19651  opprlemOLD  19783  sralemOLD  20355  srasca  20362  sravsca  20363  znbaslemOLD  20655  thlbas  20813  thlle  20814  opsrbaslemOLD  21161  matsca  21472  tuslemOLD  23327  setsmsbas  23536  setsmsds  23537  tngdsOLD  23718  ttgval  27140  ttglemOLD  27142  cchhllemOLD  27158  axlowdimlem6  27218  zlmds  31814  zlmtset  31815  nosepne  33810  hlhilslemOLD  39880  zlmodzxzldeplem  45727  line2  45986  prstcleval  46237  prstcocval  46239