Theorem neeq12i 2419

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

Syntax hints:   <-> wb 105   = wceq 1397   =/= wne 2402

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 619  ax-in2 620  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2403

This theorem is referenced by:  3netr3g  2436  3netr4g  2437  starvndxnbasendx  13243  starvndxnplusgndx  13244  starvndxnmulrndx  13245  scandxnbasendx  13255  scandxnplusgndx  13256  scandxnmulrndx  13257  vscandxnbasendx  13260  vscandxnplusgndx  13261  vscandxnmulrndx  13262  vscandxnscandx  13263  ipndxnbasendx  13273  ipndxnplusgndx  13274  ipndxnmulrndx  13275  slotsdifipndx  13276  tsetndxnplusgndx  13293  tsetndxnmulrndx  13294  tsetndxnstarvndx  13295  slotstnscsi  13296  plendxnplusgndx  13307  plendxnmulrndx  13308  plendxnscandx  13309  plendxnvscandx  13310  slotsdifplendx  13311  basendxnocndx  13314  plendxnocndx  13315  dsndxnplusgndx  13322  dsndxnmulrndx  13323  slotsdnscsi  13324  dsndxntsetndx  13325  slotsdifdsndx  13326  unifndxntsetndx  13332  slotsdifunifndx  13333  setsmsbasg  15222  setsmsdsg  15223