Theorem neeq12i 2419

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 2418	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐴 ≠ 𝐷)
3		neeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
4	3	neeq1i 2417	. 2 ⊢ (𝐴 ≠ 𝐷 ↔ 𝐵 ≠ 𝐷)
5	2, 4	bitri 184	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

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  13230  starvndxnplusgndx  13231  starvndxnmulrndx  13232  scandxnbasendx  13242  scandxnplusgndx  13243  scandxnmulrndx  13244  vscandxnbasendx  13247  vscandxnplusgndx  13248  vscandxnmulrndx  13249  vscandxnscandx  13250  ipndxnbasendx  13260  ipndxnplusgndx  13261  ipndxnmulrndx  13262  slotsdifipndx  13263  tsetndxnplusgndx  13280  tsetndxnmulrndx  13281  tsetndxnstarvndx  13282  slotstnscsi  13283  plendxnplusgndx  13294  plendxnmulrndx  13295  plendxnscandx  13296  plendxnvscandx  13297  slotsdifplendx  13298  basendxnocndx  13301  plendxnocndx  13302  dsndxnplusgndx  13309  dsndxnmulrndx  13310  slotsdnscsi  13311  dsndxntsetndx  13312  slotsdifdsndx  13313  unifndxntsetndx  13319  slotsdifunifndx  13320  setsmsbasg  15209  setsmsdsg  15210