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  13175  starvndxnplusgndx  13176  starvndxnmulrndx  13177  scandxnbasendx  13187  scandxnplusgndx  13188  scandxnmulrndx  13189  vscandxnbasendx  13192  vscandxnplusgndx  13193  vscandxnmulrndx  13194  vscandxnscandx  13195  ipndxnbasendx  13205  ipndxnplusgndx  13206  ipndxnmulrndx  13207  slotsdifipndx  13208  tsetndxnplusgndx  13225  tsetndxnmulrndx  13226  tsetndxnstarvndx  13227  slotstnscsi  13228  plendxnplusgndx  13239  plendxnmulrndx  13240  plendxnscandx  13241  plendxnvscandx  13242  slotsdifplendx  13243  basendxnocndx  13246  plendxnocndx  13247  dsndxnplusgndx  13254  dsndxnmulrndx  13255  slotsdnscsi  13256  dsndxntsetndx  13257  slotsdifdsndx  13258  unifndxntsetndx  13264  slotsdifunifndx  13265  setsmsbasg  15153  setsmsdsg  15154