Theorem neeq12i 2419

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

Syntax hints:   ↔ wb 105   = wceq 1397   ≠ wne 2402

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3netr3g  2436  3netr4g  2437  starvndxnbasendx  13224  starvndxnplusgndx  13225  starvndxnmulrndx  13226  scandxnbasendx  13236  scandxnplusgndx  13237  scandxnmulrndx  13238  vscandxnbasendx  13241  vscandxnplusgndx  13242  vscandxnmulrndx  13243  vscandxnscandx  13244  ipndxnbasendx  13254  ipndxnplusgndx  13255  ipndxnmulrndx  13256  slotsdifipndx  13257  tsetndxnplusgndx  13274  tsetndxnmulrndx  13275  tsetndxnstarvndx  13276  slotstnscsi  13277  plendxnplusgndx  13288  plendxnmulrndx  13289  plendxnscandx  13290  plendxnvscandx  13291  slotsdifplendx  13292  basendxnocndx  13295  plendxnocndx  13296  dsndxnplusgndx  13303  dsndxnmulrndx  13304  slotsdnscsi  13305  dsndxntsetndx  13306  slotsdifdsndx  13307  unifndxntsetndx  13313  slotsdifunifndx  13314  setsmsbasg  15202  setsmsdsg  15203