Theorem neeq12i 2756

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

Syntax hints:   <-> wb 184   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  3netr3g  2774  3netr4g  2775  oppchomfval  14970  oppcbas  14974  rescbas  15059  rescco  15062  rescabs  15063  odubas  15620  oppglem  16190  mgplem  16948  mgpress  16954  opprlem  17078  sralem  17623  srasca  17627  sravsca  17628  opsrbaslem  17941  zlmsca  18353  znbaslem  18372  thlbas  18522  thlle  18523  matsca  18712  tuslem  20533  setsmsbas  20741  setsmsds  20742  tngds  20925  ttgval  23882  ttglem  23883  cchhllem  23894  axlowdimlem6  23954  zlmds  27609  zlmtset  27610  zlmodzxzldeplem  32198  hlhilslem  36756