Theorem neeq12i 3001

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 2987	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Syntax hints:   ↔ wb 209   = wceq 1542   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2731  df-ne 2936

This theorem is referenced by:  3netr3g  3013  3netr4g  3014  oppchomfval  17101  oppcbas  17105  rescbas  17217  rescco  17220  rescabs  17221  odubas  17872  oppglem  18609  mgplem  19376  mgpress  19382  opprlem  19513  sralem  20081  srasca  20085  sravsca  20086  zlmsca  20354  znbaslem  20370  thlbas  20525  thlle  20526  opsrbaslem  20873  matsca  21179  tuslem  23032  setsmsbas  23241  setsmsds  23242  tngds  23414  ttgval  26834  ttglem  26835  cchhllem  26846  axlowdimlem6  26906  zlmds  31497  zlmtset  31498  nosepne  33539  hlhilslem  39608  zlmodzxzldeplem  45421  line2  45680  prstcleval  45856  prstcocval  45858