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  13545  starvndxnplusgndx  13546  starvndxnmulrndx  13547  scandxnbasendx  13557  scandxnplusgndx  13558  scandxnmulrndx  13559  vscandxnbasendx  13562  vscandxnplusgndx  13563  vscandxnmulrndx  13564  vscandxnscandx  13565  ipndxnbasendx  13575  ipndxnplusgndx  13576  ipndxnmulrndx  13577  slotsdifipndx  13578  tsetndxnplusgndx  13595  tsetndxnmulrndx  13596  tsetndxnstarvndx  13597  slotstnscsi  13598  plendxnplusgndx  13609  plendxnmulrndx  13610  plendxnscandx  13611  plendxnvscandx  13612  slotsdifplendx  13613  basendxnocndx  13616  plendxnocndx  13617  dsndxnplusgndx  13624  dsndxnmulrndx  13625  slotsdnscsi  13626  dsndxntsetndx  13627  slotsdifdsndx  13628  unifndxntsetndx  13634  slotsdifunifndx  13635  setsmsbasg  15629  setsmsdsg  15630