Theorem neeq12i 2364

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

Syntax hints:   <-> wb 105   = wceq 1353   =/= wne 2347

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  3netr3g  2381  3netr4g  2382  scandxnbasendx  12574  scandxnplusgndx  12575  scandxnmulrndx  12576  tsetndxnplusgndx  12601  tsetndxnmulrndx  12602  tsetndxnstarvndx  12603  slotstnscsi  12604  dsndxnplusgndx  12618  dsndxnmulrndx  12619  slotsdnscsi  12620  dsndxntsetndx  12621  slotsdifdsndx  12622  setsmsbasg  13612  setsmsdsg  13613