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  13007  starvndxnplusgndx  13008  starvndxnmulrndx  13009  scandxnbasendx  13019  scandxnplusgndx  13020  scandxnmulrndx  13021  vscandxnbasendx  13024  vscandxnplusgndx  13025  vscandxnmulrndx  13026  vscandxnscandx  13027  ipndxnbasendx  13037  ipndxnplusgndx  13038  ipndxnmulrndx  13039  slotsdifipndx  13040  tsetndxnplusgndx  13057  tsetndxnmulrndx  13058  tsetndxnstarvndx  13059  slotstnscsi  13060  plendxnplusgndx  13071  plendxnmulrndx  13072  plendxnscandx  13073  plendxnvscandx  13074  slotsdifplendx  13075  basendxnocndx  13078  plendxnocndx  13079  dsndxnplusgndx  13086  dsndxnmulrndx  13087  slotsdnscsi  13088  dsndxntsetndx  13089  slotsdifdsndx  13090  unifndxntsetndx  13096  slotsdifunifndx  13097  setsmsbasg  14984  setsmsdsg  14985