Theorem neeq12i 3026

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ne 2961

This theorem is used by:  3netr3g  3038  3netr4g  3039  starvndxnbasendx  17379  starvndxnplusgndx  17380  starvndxnmulrndx  17381  scandxnbasendx  17391  scandxnplusgndx  17392  scandxnmulrndx  17393  vscandxnbasendx  17396  vscandxnplusgndx  17397  vscandxnmulrndx  17398  vscandxnscandx  17399  ipndxnbasendx  17407  ipndxnplusgndx  17408  ipndxnmulrndx  17409  slotsdifipndx  17410  tsetndxnplusgndx  17432  tsetndxnmulrndx  17433  tsetndxnstarvndx  17434  slotstnscsi  17435  plendxnplusgndx  17446  plendxnmulrndx  17447  plendxnscandx  17448  plendxnvscandx  17449  slotsdifplendx  17450  basendxnocndx  17458  plendxnocndx  17459  dsndxnplusgndx  17465  dsndxnmulrndx  17466  slotsdnscsi  17467  dsndxntsetndx  17468  slotsdifdsndx  17469  unifndxntsetndx  17475  slotsdifunifndx  17476  slotsdifplendx2  17491  slotsdifocndx  17492  nosepne  27895  lngndxnitvndx  28763  axlowdimlem6  29352  oaomoencom  44102  gpgprismgr4cycllem7  48924  zlmodzxzldeplem  49335  line2  49589