Theorem neeq12i 2431

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

Syntax hints:   <-> wb 105   = wceq 1398   =/= wne 2414

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  3netr3g  2448  3netr4g  2449  starvndxnbasendx  13372  starvndxnplusgndx  13373  starvndxnmulrndx  13374  scandxnbasendx  13384  scandxnplusgndx  13385  scandxnmulrndx  13386  vscandxnbasendx  13389  vscandxnplusgndx  13390  vscandxnmulrndx  13391  vscandxnscandx  13392  ipndxnbasendx  13402  ipndxnplusgndx  13403  ipndxnmulrndx  13404  slotsdifipndx  13405  tsetndxnplusgndx  13422  tsetndxnmulrndx  13423  tsetndxnstarvndx  13424  slotstnscsi  13425  plendxnplusgndx  13436  plendxnmulrndx  13437  plendxnscandx  13438  plendxnvscandx  13439  slotsdifplendx  13440  basendxnocndx  13443  plendxnocndx  13444  dsndxnplusgndx  13451  dsndxnmulrndx  13452  slotsdnscsi  13453  dsndxntsetndx  13454  slotsdifdsndx  13455  unifndxntsetndx  13461  slotsdifunifndx  13462  setsmsbasg  15361  setsmsdsg  15362