Theorem neeq12i 2420

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

Syntax hints:   ↔ wb 105   = wceq 1398   ≠ wne 2403

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2404

This theorem is referenced by:  3netr3g  2437  3netr4g  2438  starvndxnbasendx  13288  starvndxnplusgndx  13289  starvndxnmulrndx  13290  scandxnbasendx  13300  scandxnplusgndx  13301  scandxnmulrndx  13302  vscandxnbasendx  13305  vscandxnplusgndx  13306  vscandxnmulrndx  13307  vscandxnscandx  13308  ipndxnbasendx  13318  ipndxnplusgndx  13319  ipndxnmulrndx  13320  slotsdifipndx  13321  tsetndxnplusgndx  13338  tsetndxnmulrndx  13339  tsetndxnstarvndx  13340  slotstnscsi  13341  plendxnplusgndx  13352  plendxnmulrndx  13353  plendxnscandx  13354  plendxnvscandx  13355  slotsdifplendx  13356  basendxnocndx  13359  plendxnocndx  13360  dsndxnplusgndx  13367  dsndxnmulrndx  13368  slotsdnscsi  13369  dsndxntsetndx  13370  slotsdifdsndx  13371  unifndxntsetndx  13377  slotsdifunifndx  13378  setsmsbasg  15273  setsmsdsg  15274