Theorem neeq12i 2437

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

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  3netr3g  2454  3netr4g  2455  starvndxnbasendx  13555  starvndxnplusgndx  13556  starvndxnmulrndx  13557  scandxnbasendx  13567  scandxnplusgndx  13568  scandxnmulrndx  13569  vscandxnbasendx  13572  vscandxnplusgndx  13573  vscandxnmulrndx  13574  vscandxnscandx  13575  ipndxnbasendx  13585  ipndxnplusgndx  13586  ipndxnmulrndx  13587  slotsdifipndx  13588  tsetndxnplusgndx  13605  tsetndxnmulrndx  13606  tsetndxnstarvndx  13607  slotstnscsi  13608  plendxnplusgndx  13619  plendxnmulrndx  13620  plendxnscandx  13621  plendxnvscandx  13622  slotsdifplendx  13623  basendxnocndx  13626  plendxnocndx  13627  dsndxnplusgndx  13634  dsndxnmulrndx  13635  slotsdnscsi  13636  dsndxntsetndx  13637  slotsdifdsndx  13638  unifndxntsetndx  13644  slotsdifunifndx  13645  setsmsbasg  15705  setsmsdsg  15706