Theorem neeq12i 2417

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

Syntax hints:   <-> wb 105   = wceq 1395   =/= wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  3netr3g  2434  3netr4g  2435  starvndxnbasendx  13191  starvndxnplusgndx  13192  starvndxnmulrndx  13193  scandxnbasendx  13203  scandxnplusgndx  13204  scandxnmulrndx  13205  vscandxnbasendx  13208  vscandxnplusgndx  13209  vscandxnmulrndx  13210  vscandxnscandx  13211  ipndxnbasendx  13221  ipndxnplusgndx  13222  ipndxnmulrndx  13223  slotsdifipndx  13224  tsetndxnplusgndx  13241  tsetndxnmulrndx  13242  tsetndxnstarvndx  13243  slotstnscsi  13244  plendxnplusgndx  13255  plendxnmulrndx  13256  plendxnscandx  13257  plendxnvscandx  13258  slotsdifplendx  13259  basendxnocndx  13262  plendxnocndx  13263  dsndxnplusgndx  13270  dsndxnmulrndx  13271  slotsdnscsi  13272  dsndxntsetndx  13273  slotsdifdsndx  13274  unifndxntsetndx  13280  slotsdifunifndx  13281  setsmsbasg  15169  setsmsdsg  15170