Theorem neeq12i 2713

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 2442	. 2 |- ( A = C <-> B = D )
4	3	necon3bii 2692	1 |- ( A =/= C <-> B =/= D )

Syntax hints:   <-> wb 187   = wceq 1437   =/= wne 2618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2620

This theorem is referenced by:  3netr3g  2731  3netr4g  2732  oppchomfval  15607  oppcbas  15611  rescbas  15722  rescco  15725  rescabs  15726  odubas  16367  oppglem  16989  mgplem  17716  mgpress  17722  opprlem  17844  sralem  18388  srasca  18392  sravsca  18393  opsrbaslem  18689  zlmsca  19079  znbaslem  19096  thlbas  19246  thlle  19247  matsca  19427  tuslem  21269  setsmsbas  21477  setsmsds  21478  tngds  21643  ttgval  24892  ttglem  24893  cchhllem  24904  axlowdimlem6  24964  zlmds  28764  zlmtset  28765  hlhilslem  35428  zlmodzxzldeplem  39565