Theorem neeq12i 2437

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

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  3netr3g  2454  3netr4g  2455  starvndxnbasendx  13549  starvndxnplusgndx  13550  starvndxnmulrndx  13551  scandxnbasendx  13561  scandxnplusgndx  13562  scandxnmulrndx  13563  vscandxnbasendx  13566  vscandxnplusgndx  13567  vscandxnmulrndx  13568  vscandxnscandx  13569  ipndxnbasendx  13579  ipndxnplusgndx  13580  ipndxnmulrndx  13581  slotsdifipndx  13582  tsetndxnplusgndx  13599  tsetndxnmulrndx  13600  tsetndxnstarvndx  13601  slotstnscsi  13602  plendxnplusgndx  13613  plendxnmulrndx  13614  plendxnscandx  13615  plendxnvscandx  13616  slotsdifplendx  13617  basendxnocndx  13620  plendxnocndx  13621  dsndxnplusgndx  13628  dsndxnmulrndx  13629  slotsdnscsi  13630  dsndxntsetndx  13631  slotsdifdsndx  13632  unifndxntsetndx  13638  slotsdifunifndx  13639  setsmsbasg  15671  setsmsdsg  15672