Theorem neeq12i 2998

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

Syntax hints:   ↔ wb 206   = wceq 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  3netr3g  3010  3netr4g  3011  starvndxnbasendx  17224  starvndxnplusgndx  17225  starvndxnmulrndx  17226  scandxnbasendx  17236  scandxnplusgndx  17237  scandxnmulrndx  17238  vscandxnbasendx  17241  vscandxnplusgndx  17242  vscandxnmulrndx  17243  vscandxnscandx  17244  ipndxnbasendx  17252  ipndxnplusgndx  17253  ipndxnmulrndx  17254  slotsdifipndx  17255  tsetndxnplusgndx  17277  tsetndxnmulrndx  17278  tsetndxnstarvndx  17279  slotstnscsi  17280  plendxnplusgndx  17291  plendxnmulrndx  17292  plendxnscandx  17293  plendxnvscandx  17294  slotsdifplendx  17295  basendxnocndx  17303  plendxnocndx  17304  dsndxnplusgndx  17310  dsndxnmulrndx  17311  slotsdnscsi  17312  dsndxntsetndx  17313  slotsdifdsndx  17314  unifndxntsetndx  17320  slotsdifunifndx  17321  slotsdifplendx2  17336  slotsdifocndx  17337  nosepne  27648  lngndxnitvndx  28515  axlowdimlem6  29020  oaomoencom  43559  gpgprismgr4cycllem7  48347  zlmodzxzldeplem  48744  line2  48998