Theorem neeq12i 2437

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

Syntax hints:   ↔ wb 105   = wceq 1402   ≠ wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  3netr3g  2454  3netr4g  2455  starvndxnbasendx  13473  starvndxnplusgndx  13474  starvndxnmulrndx  13475  scandxnbasendx  13485  scandxnplusgndx  13486  scandxnmulrndx  13487  vscandxnbasendx  13490  vscandxnplusgndx  13491  vscandxnmulrndx  13492  vscandxnscandx  13493  ipndxnbasendx  13503  ipndxnplusgndx  13504  ipndxnmulrndx  13505  slotsdifipndx  13506  tsetndxnplusgndx  13523  tsetndxnmulrndx  13524  tsetndxnstarvndx  13525  slotstnscsi  13526  plendxnplusgndx  13537  plendxnmulrndx  13538  plendxnscandx  13539  plendxnvscandx  13540  slotsdifplendx  13541  basendxnocndx  13544  plendxnocndx  13545  dsndxnplusgndx  13552  dsndxnmulrndx  13553  slotsdnscsi  13554  dsndxntsetndx  13555  slotsdifdsndx  13556  unifndxntsetndx  13562  slotsdifunifndx  13563  setsmsbasg  15503  setsmsdsg  15504