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  12762  starvndxnplusgndx  12763  starvndxnmulrndx  12764  scandxnbasendx  12774  scandxnplusgndx  12775  scandxnmulrndx  12776  vscandxnbasendx  12779  vscandxnplusgndx  12780  vscandxnmulrndx  12781  vscandxnscandx  12782  ipndxnbasendx  12792  ipndxnplusgndx  12793  ipndxnmulrndx  12794  slotsdifipndx  12795  tsetndxnplusgndx  12812  tsetndxnmulrndx  12813  tsetndxnstarvndx  12814  slotstnscsi  12815  plendxnplusgndx  12826  plendxnmulrndx  12827  plendxnscandx  12828  plendxnvscandx  12829  slotsdifplendx  12830  dsndxnplusgndx  12837  dsndxnmulrndx  12838  slotsdnscsi  12839  dsndxntsetndx  12840  slotsdifdsndx  12841  unifndxntsetndx  12847  slotsdifunifndx  12848  setsmsbasg  14658  setsmsdsg  14659