Theorem neeq12i 2364

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.)

Hypotheses

Ref	Expression
neeq1i.1	⊢ 𝐴 = 𝐵
neeq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
neeq12i	⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Proof of Theorem neeq12i

Step	Hyp	Ref	Expression
1		neeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
2	1	neeq2i 2363	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐴 ≠ 𝐷)
3		neeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
4	3	neeq1i 2362	. 2 ⊢ (𝐴 ≠ 𝐷 ↔ 𝐵 ≠ 𝐷)
5	2, 4	bitri 184	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

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  starvndxnbasendx  12602  starvndxnplusgndx  12603  starvndxnmulrndx  12604  scandxnbasendx  12614  scandxnplusgndx  12615  scandxnmulrndx  12616  vscandxnbasendx  12619  vscandxnplusgndx  12620  vscandxnmulrndx  12621  vscandxnscandx  12622  ipndxnbasendx  12632  ipndxnplusgndx  12633  ipndxnmulrndx  12634  slotsdifipndx  12635  tsetndxnplusgndx  12652  tsetndxnmulrndx  12653  tsetndxnstarvndx  12654  slotstnscsi  12655  plendxnplusgndx  12666  plendxnmulrndx  12667  plendxnscandx  12668  plendxnvscandx  12669  slotsdifplendx  12670  dsndxnplusgndx  12677  dsndxnmulrndx  12678  slotsdnscsi  12679  dsndxntsetndx  12680  slotsdifdsndx  12681  unifndxntsetndx  12687  slotsdifunifndx  12688  setsmsbasg  14064  setsmsdsg  14065