Theorem neeq12i 2732

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

Syntax hints:   <-> wb 184   = wceq 1383   =/= wne 2638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640

This theorem is referenced by:  3netr3g  2750  3netr4g  2751  oppchomfval  14986  oppcbas  14990  rescbas  15075  rescco  15078  rescabs  15079  odubas  15637  oppglem  16259  mgplem  17020  mgpress  17026  opprlem  17151  sralem  17697  srasca  17701  sravsca  17702  opsrbaslem  18016  zlmsca  18431  znbaslem  18450  thlbas  18600  thlle  18601  matsca  18790  tuslem  20643  setsmsbas  20851  setsmsds  20852  tngds  21035  ttgval  24050  ttglem  24051  cchhllem  24062  axlowdimlem6  24122  zlmds  27818  zlmtset  27819  zlmodzxzldeplem  32834  hlhilslem  37408