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  13554  starvndxnplusgndx  13555  starvndxnmulrndx  13556  scandxnbasendx  13566  scandxnplusgndx  13567  scandxnmulrndx  13568  vscandxnbasendx  13571  vscandxnplusgndx  13572  vscandxnmulrndx  13573  vscandxnscandx  13574  ipndxnbasendx  13584  ipndxnplusgndx  13585  ipndxnmulrndx  13586  slotsdifipndx  13587  tsetndxnplusgndx  13604  tsetndxnmulrndx  13605  tsetndxnstarvndx  13606  slotstnscsi  13607  plendxnplusgndx  13618  plendxnmulrndx  13619  plendxnscandx  13620  plendxnvscandx  13621  slotsdifplendx  13622  basendxnocndx  13625  plendxnocndx  13626  dsndxnplusgndx  13633  dsndxnmulrndx  13634  slotsdnscsi  13635  dsndxntsetndx  13636  slotsdifdsndx  13637  unifndxntsetndx  13643  slotsdifunifndx  13644  setsmsbasg  15722  setsmsdsg  15723