Theorem neeq12i 2395

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

Syntax hints:   <-> wb 105   = wceq 1373   =/= wne 2378

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-ne 2379

This theorem is referenced by:  3netr3g  2412  3netr4g  2413  starvndxnbasendx  13089  starvndxnplusgndx  13090  starvndxnmulrndx  13091  scandxnbasendx  13101  scandxnplusgndx  13102  scandxnmulrndx  13103  vscandxnbasendx  13106  vscandxnplusgndx  13107  vscandxnmulrndx  13108  vscandxnscandx  13109  ipndxnbasendx  13119  ipndxnplusgndx  13120  ipndxnmulrndx  13121  slotsdifipndx  13122  tsetndxnplusgndx  13139  tsetndxnmulrndx  13140  tsetndxnstarvndx  13141  slotstnscsi  13142  plendxnplusgndx  13153  plendxnmulrndx  13154  plendxnscandx  13155  plendxnvscandx  13156  slotsdifplendx  13157  basendxnocndx  13160  plendxnocndx  13161  dsndxnplusgndx  13168  dsndxnmulrndx  13169  slotsdnscsi  13170  dsndxntsetndx  13171  slotsdifdsndx  13172  unifndxntsetndx  13178  slotsdifunifndx  13179  setsmsbasg  15066  setsmsdsg  15067