Theorem neeq12i 2384

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  3netr3g  2401  3netr4g  2402  starvndxnbasendx  12844  starvndxnplusgndx  12845  starvndxnmulrndx  12846  scandxnbasendx  12856  scandxnplusgndx  12857  scandxnmulrndx  12858  vscandxnbasendx  12861  vscandxnplusgndx  12862  vscandxnmulrndx  12863  vscandxnscandx  12864  ipndxnbasendx  12874  ipndxnplusgndx  12875  ipndxnmulrndx  12876  slotsdifipndx  12877  tsetndxnplusgndx  12894  tsetndxnmulrndx  12895  tsetndxnstarvndx  12896  slotstnscsi  12897  plendxnplusgndx  12908  plendxnmulrndx  12909  plendxnscandx  12910  plendxnvscandx  12911  slotsdifplendx  12912  basendxnocndx  12915  plendxnocndx  12916  dsndxnplusgndx  12923  dsndxnmulrndx  12924  slotsdnscsi  12925  dsndxntsetndx  12926  slotsdifdsndx  12927  unifndxntsetndx  12933  slotsdifunifndx  12934  setsmsbasg  14799  setsmsdsg  14800