Theorem neeq12i 2860

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

Syntax hints:   <-> wb 196   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  3netr3g  2872  3netr4g  2873  oppchomfval  16374  oppcbas  16378  rescbas  16489  rescco  16492  rescabs  16493  odubas  17133  oppglem  17780  mgplem  18494  mgpress  18500  opprlem  18628  sralem  19177  srasca  19181  sravsca  19182  opsrbaslem  19477  opsrbaslemOLD  19478  zlmsca  19869  znbaslem  19886  znbaslemOLD  19887  thlbas  20040  thlle  20041  matsca  20221  tuslem  22071  setsmsbas  22280  setsmsds  22281  tngds  22452  ttgval  25755  ttglem  25756  cchhllem  25767  axlowdimlem6  25827  zlmds  30008  zlmtset  30009  nosepne  31831  hlhilslem  37230  zlmodzxzldeplem  42287