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

Syntax hints:   ↔ wb 196   = wceq 1631   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-ne 2944

This theorem is referenced by:  3netr3g  3021  3netr4g  3022  oppchomfval  16581  oppcbas  16585  rescbas  16696  rescco  16699  rescabs  16700  odubas  17341  oppglem  17987  mgplem  18702  mgpress  18708  opprlem  18836  sralem  19392  srasca  19396  sravsca  19397  opsrbaslem  19692  opsrbaslemOLD  19693  zlmsca  20084  znbaslem  20101  znbaslemOLD  20102  thlbas  20257  thlle  20258  matsca  20438  tuslem  22291  setsmsbas  22500  setsmsds  22501  tngds  22672  ttgval  25976  ttglem  25977  cchhllem  25988  axlowdimlem6  26048  zlmds  30348  zlmtset  30349  nosepne  32168  hlhilslem  37748  zlmodzxzldeplem  42815