Theorem neeq12i 2393

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

Syntax hints:   <-> wb 105   = wceq 1373   =/= wne 2376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-ne 2377

This theorem is referenced by:  3netr3g  2410  3netr4g  2411  starvndxnbasendx  12974  starvndxnplusgndx  12975  starvndxnmulrndx  12976  scandxnbasendx  12986  scandxnplusgndx  12987  scandxnmulrndx  12988  vscandxnbasendx  12991  vscandxnplusgndx  12992  vscandxnmulrndx  12993  vscandxnscandx  12994  ipndxnbasendx  13004  ipndxnplusgndx  13005  ipndxnmulrndx  13006  slotsdifipndx  13007  tsetndxnplusgndx  13024  tsetndxnmulrndx  13025  tsetndxnstarvndx  13026  slotstnscsi  13027  plendxnplusgndx  13038  plendxnmulrndx  13039  plendxnscandx  13040  plendxnvscandx  13041  slotsdifplendx  13042  basendxnocndx  13045  plendxnocndx  13046  dsndxnplusgndx  13053  dsndxnmulrndx  13054  slotsdnscsi  13055  dsndxntsetndx  13056  slotsdifdsndx  13057  unifndxntsetndx  13063  slotsdifunifndx  13064  setsmsbasg  14951  setsmsdsg  14952