Theorem neeq12i 2392

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

Syntax hints:   ↔ wb 105   = wceq 1372   ≠ wne 2375

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-ne 2376

This theorem is referenced by:  3netr3g  2409  3netr4g  2410  starvndxnbasendx  12892  starvndxnplusgndx  12893  starvndxnmulrndx  12894  scandxnbasendx  12904  scandxnplusgndx  12905  scandxnmulrndx  12906  vscandxnbasendx  12909  vscandxnplusgndx  12910  vscandxnmulrndx  12911  vscandxnscandx  12912  ipndxnbasendx  12922  ipndxnplusgndx  12923  ipndxnmulrndx  12924  slotsdifipndx  12925  tsetndxnplusgndx  12942  tsetndxnmulrndx  12943  tsetndxnstarvndx  12944  slotstnscsi  12945  plendxnplusgndx  12956  plendxnmulrndx  12957  plendxnscandx  12958  plendxnvscandx  12959  slotsdifplendx  12960  basendxnocndx  12963  plendxnocndx  12964  dsndxnplusgndx  12971  dsndxnmulrndx  12972  slotsdnscsi  12973  dsndxntsetndx  12974  slotsdifdsndx  12975  unifndxntsetndx  12981  slotsdifunifndx  12982  setsmsbasg  14869  setsmsdsg  14870