Theorem neeq12i 3053

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

Syntax hints:   ↔ wb 209   = wceq 1538   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  3netr3g  3065  3netr4g  3066  oppchomfval  16976  oppcbas  16980  rescbas  17091  rescco  17094  rescabs  17095  odubas  17735  oppglem  18470  mgplem  19237  mgpress  19243  opprlem  19374  sralem  19942  srasca  19946  sravsca  19947  zlmsca  20214  znbaslem  20230  thlbas  20385  thlle  20386  opsrbaslem  20717  matsca  21020  tuslem  22873  setsmsbas  23082  setsmsds  23083  tngds  23254  ttgval  26669  ttglem  26670  cchhllem  26681  axlowdimlem6  26741  zlmds  31315  zlmtset  31316  nosepne  33298  hlhilslem  39234  zlmodzxzldeplem  44907  line2  45166