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  13227  starvndxnplusgndx  13228  starvndxnmulrndx  13229  scandxnbasendx  13239  scandxnplusgndx  13240  scandxnmulrndx  13241  vscandxnbasendx  13244  vscandxnplusgndx  13245  vscandxnmulrndx  13246  vscandxnscandx  13247  ipndxnbasendx  13257  ipndxnplusgndx  13258  ipndxnmulrndx  13259  slotsdifipndx  13260  tsetndxnplusgndx  13277  tsetndxnmulrndx  13278  tsetndxnstarvndx  13279  slotstnscsi  13280  plendxnplusgndx  13291  plendxnmulrndx  13292  plendxnscandx  13293  plendxnvscandx  13294  slotsdifplendx  13295  basendxnocndx  13298  plendxnocndx  13299  dsndxnplusgndx  13306  dsndxnmulrndx  13307  slotsdnscsi  13308  dsndxntsetndx  13309  slotsdifdsndx  13310  unifndxntsetndx  13316  slotsdifunifndx  13317  setsmsbasg  15206  setsmsdsg  15207