Theorem neeq12i 2992

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

Syntax hints:   ↔ wb 206   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  3netr3g  3004  3netr4g  3005  starvndxnbasendx  17274  starvndxnplusgndx  17275  starvndxnmulrndx  17276  scandxnbasendx  17286  scandxnplusgndx  17287  scandxnmulrndx  17288  vscandxnbasendx  17291  vscandxnplusgndx  17292  vscandxnmulrndx  17293  vscandxnscandx  17294  ipndxnbasendx  17302  ipndxnplusgndx  17303  ipndxnmulrndx  17304  slotsdifipndx  17305  tsetndxnplusgndx  17327  tsetndxnmulrndx  17328  tsetndxnstarvndx  17329  slotstnscsi  17330  plendxnplusgndx  17341  plendxnmulrndx  17342  plendxnscandx  17343  plendxnvscandx  17344  slotsdifplendx  17345  basendxnocndx  17353  plendxnocndx  17354  dsndxnplusgndx  17360  dsndxnmulrndx  17361  slotsdnscsi  17362  dsndxntsetndx  17363  slotsdifdsndx  17364  unifndxntsetndx  17370  slotsdifunifndx  17371  slotsdifplendx2  17386  slotsdifocndx  17387  nosepne  27599  lngndxnitvndx  28377  axlowdimlem6  28881  oaomoencom  43313  gpgprismgr4cycllem7  48095  zlmodzxzldeplem  48491  line2  48745