Theorem neeq12i 2381

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

Syntax hints:   <-> wb 105   = wceq 1364   =/= wne 2364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  3netr3g  2398  3netr4g  2399  starvndxnbasendx  12759  starvndxnplusgndx  12760  starvndxnmulrndx  12761  scandxnbasendx  12771  scandxnplusgndx  12772  scandxnmulrndx  12773  vscandxnbasendx  12776  vscandxnplusgndx  12777  vscandxnmulrndx  12778  vscandxnscandx  12779  ipndxnbasendx  12789  ipndxnplusgndx  12790  ipndxnmulrndx  12791  slotsdifipndx  12792  tsetndxnplusgndx  12809  tsetndxnmulrndx  12810  tsetndxnstarvndx  12811  slotstnscsi  12812  plendxnplusgndx  12823  plendxnmulrndx  12824  plendxnscandx  12825  plendxnvscandx  12826  slotsdifplendx  12827  dsndxnplusgndx  12834  dsndxnmulrndx  12835  slotsdnscsi  12836  dsndxntsetndx  12837  slotsdifdsndx  12838  unifndxntsetndx  12844  slotsdifunifndx  12845  setsmsbasg  14647  setsmsdsg  14648