Theorem neeq12i 2620

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.)

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		neeq12i.2	. . 3 |- C = D
2	1	neeq2i 2619	. 2 |- ( A =/= C <-> A =/= D )
3		neeq1i.1	. . 3 |- A = B
4	3	neeq1i 2618	. 2 |- ( A =/= D <-> B =/= D )
5	2, 4	bitri 249	1 |- ( A =/= C <-> B =/= D )

Syntax hints:   <-> wb 184   = wceq 1369   =/= wne 2606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-ne 2608

This theorem is referenced by:  3netr3g  2636  3netr4g  2637  oppchomfval  14653  oppcbas  14657  rescbas  14742  rescco  14745  rescabs  14746  odubas  15303  oppglem  15865  mgplem  16596  mgpress  16602  opprlem  16720  sralem  17258  srasca  17262  sravsca  17263  opsrbaslem  17559  zlmsca  17952  znbaslem  17971  thlbas  18121  thlle  18122  matsca  18316  tuslem  19842  setsmsbas  20050  setsmsds  20051  tngds  20234  ttgval  23121  ttglem  23122  cchhllem  23133  axlowdimlem6  23193  zlmds  26393  zlmtset  26394  zlmodzxzldeplem  31040  hlhilslem  35586