Theorem neeq12i 2690

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypotheses

Ref	Expression
neeq1i.1	|- A = B
neeq12i.2	|- C = D

Assertion

Ref	Expression
neeq12i	|- ( A =/= C <-> B =/= D )

Proof of Theorem neeq12i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 |- A = B
2		neeq12i.2	. . 3 |- C = D
3	1, 2	eqeq12i 2465	. 2 |- ( A = C <-> B = D )
4	3	necon3bii 2676	1 |- ( A =/= C <-> B =/= D )

Syntax hints:   <-> wb 188   = wceq 1444   =/= wne 2622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624

This theorem is referenced by:  3netr3g  2702  3netr4g  2703  oppchomfval  15619  oppcbas  15623  rescbas  15734  rescco  15737  rescabs  15738  odubas  16379  oppglem  17001  mgplem  17728  mgpress  17734  opprlem  17856  sralem  18400  srasca  18404  sravsca  18405  opsrbaslem  18701  zlmsca  19092  znbaslem  19109  thlbas  19259  thlle  19260  matsca  19440  tuslem  21282  setsmsbas  21490  setsmsds  21491  tngds  21656  ttgval  24905  ttglem  24906  cchhllem  24917  axlowdimlem6  24977  zlmds  28768  zlmtset  28769  hlhilslem  35509  zlmodzxzldeplem  40344