Theorem neeq12i 2431

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  3netr3g  2448  3netr4g  2449  starvndxnbasendx  13439  starvndxnplusgndx  13440  starvndxnmulrndx  13441  scandxnbasendx  13451  scandxnplusgndx  13452  scandxnmulrndx  13453  vscandxnbasendx  13456  vscandxnplusgndx  13457  vscandxnmulrndx  13458  vscandxnscandx  13459  ipndxnbasendx  13469  ipndxnplusgndx  13470  ipndxnmulrndx  13471  slotsdifipndx  13472  tsetndxnplusgndx  13489  tsetndxnmulrndx  13490  tsetndxnstarvndx  13491  slotstnscsi  13492  plendxnplusgndx  13503  plendxnmulrndx  13504  plendxnscandx  13505  plendxnvscandx  13506  slotsdifplendx  13507  basendxnocndx  13510  plendxnocndx  13511  dsndxnplusgndx  13518  dsndxnmulrndx  13519  slotsdnscsi  13520  dsndxntsetndx  13521  slotsdifdsndx  13522  unifndxntsetndx  13528  slotsdifunifndx  13529  setsmsbasg  15470  setsmsdsg  15471