Theorem neeq12i 2420

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

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

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 2213

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

This theorem is referenced by:  3netr3g  2437  3netr4g  2438  starvndxnbasendx  13305  starvndxnplusgndx  13306  starvndxnmulrndx  13307  scandxnbasendx  13317  scandxnplusgndx  13318  scandxnmulrndx  13319  vscandxnbasendx  13322  vscandxnplusgndx  13323  vscandxnmulrndx  13324  vscandxnscandx  13325  ipndxnbasendx  13335  ipndxnplusgndx  13336  ipndxnmulrndx  13337  slotsdifipndx  13338  tsetndxnplusgndx  13355  tsetndxnmulrndx  13356  tsetndxnstarvndx  13357  slotstnscsi  13358  plendxnplusgndx  13369  plendxnmulrndx  13370  plendxnscandx  13371  plendxnvscandx  13372  slotsdifplendx  13373  basendxnocndx  13376  plendxnocndx  13377  dsndxnplusgndx  13384  dsndxnmulrndx  13385  slotsdnscsi  13386  dsndxntsetndx  13387  slotsdifdsndx  13388  unifndxntsetndx  13394  slotsdifunifndx  13395  setsmsbasg  15290  setsmsdsg  15291