Theorem neeq12i 2618

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

Syntax hints:   <-> wb 184   = wceq 1364   =/= wne 2604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434  df-ne 2606

This theorem is referenced by:  3netr3g  2634  3netr4g  2635  oppchomfval  14649  oppcbas  14653  rescbas  14738  rescco  14741  rescabs  14742  odubas  15299  oppglem  15858  mgplem  16586  mgpress  16592  opprlem  16710  sralem  17236  srasca  17240  sravsca  17241  opsrbaslem  17547  zlmsca  17852  znbaslem  17871  thlbas  18021  thlle  18022  matsca  18216  tuslem  19742  setsmsbas  19950  setsmsds  19951  tngds  20134  ttgval  23040  ttglem  23041  cchhllem  23052  axlowdimlem6  23112  zlmds  26313  zlmtset  26314  zlmodzxzldeplem  30864  hlhilslem  35274