Theorem neeq12i 2394

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

Syntax hints:   ↔ wb 105   = wceq 1373   ≠ wne 2377

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  3netr3g  2411  3netr4g  2412  starvndxnbasendx  13049  starvndxnplusgndx  13050  starvndxnmulrndx  13051  scandxnbasendx  13061  scandxnplusgndx  13062  scandxnmulrndx  13063  vscandxnbasendx  13066  vscandxnplusgndx  13067  vscandxnmulrndx  13068  vscandxnscandx  13069  ipndxnbasendx  13079  ipndxnplusgndx  13080  ipndxnmulrndx  13081  slotsdifipndx  13082  tsetndxnplusgndx  13099  tsetndxnmulrndx  13100  tsetndxnstarvndx  13101  slotstnscsi  13102  plendxnplusgndx  13113  plendxnmulrndx  13114  plendxnscandx  13115  plendxnvscandx  13116  slotsdifplendx  13117  basendxnocndx  13120  plendxnocndx  13121  dsndxnplusgndx  13128  dsndxnmulrndx  13129  slotsdnscsi  13130  dsndxntsetndx  13131  slotsdifdsndx  13132  unifndxntsetndx  13138  slotsdifunifndx  13139  setsmsbasg  15026  setsmsdsg  15027