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

Syntax hints:   ↔ wb 196   = wceq 1632   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933

This theorem is referenced by:  3netr3g  3010  3netr4g  3011  oppchomfval  16575  oppcbas  16579  rescbas  16690  rescco  16693  rescabs  16694  odubas  17334  oppglem  17980  mgplem  18694  mgpress  18700  opprlem  18828  sralem  19379  srasca  19383  sravsca  19384  opsrbaslem  19679  opsrbaslemOLD  19680  zlmsca  20071  znbaslem  20088  znbaslemOLD  20089  thlbas  20242  thlle  20243  matsca  20423  tuslem  22272  setsmsbas  22481  setsmsds  22482  tngds  22653  ttgval  25954  ttglem  25955  cchhllem  25966  axlowdimlem6  26026  zlmds  30317  zlmtset  30318  nosepne  32137  hlhilslem  37732  zlmodzxzldeplem  42797