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  13496  starvndxnplusgndx  13497  starvndxnmulrndx  13498  scandxnbasendx  13508  scandxnplusgndx  13509  scandxnmulrndx  13510  vscandxnbasendx  13513  vscandxnplusgndx  13514  vscandxnmulrndx  13515  vscandxnscandx  13516  ipndxnbasendx  13526  ipndxnplusgndx  13527  ipndxnmulrndx  13528  slotsdifipndx  13529  tsetndxnplusgndx  13546  tsetndxnmulrndx  13547  tsetndxnstarvndx  13548  slotstnscsi  13549  plendxnplusgndx  13560  plendxnmulrndx  13561  plendxnscandx  13562  plendxnvscandx  13563  slotsdifplendx  13564  basendxnocndx  13567  plendxnocndx  13568  dsndxnplusgndx  13575  dsndxnmulrndx  13576  slotsdnscsi  13577  dsndxntsetndx  13578  slotsdifdsndx  13579  unifndxntsetndx  13585  slotsdifunifndx  13586  setsmsbasg  15580  setsmsdsg  15581