Theorem neeq12i 2429

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  3netr3g  2446  3netr4g  2447  starvndxnbasendx  13355  starvndxnplusgndx  13356  starvndxnmulrndx  13357  scandxnbasendx  13367  scandxnplusgndx  13368  scandxnmulrndx  13369  vscandxnbasendx  13372  vscandxnplusgndx  13373  vscandxnmulrndx  13374  vscandxnscandx  13375  ipndxnbasendx  13385  ipndxnplusgndx  13386  ipndxnmulrndx  13387  slotsdifipndx  13388  tsetndxnplusgndx  13405  tsetndxnmulrndx  13406  tsetndxnstarvndx  13407  slotstnscsi  13408  plendxnplusgndx  13419  plendxnmulrndx  13420  plendxnscandx  13421  plendxnvscandx  13422  slotsdifplendx  13423  basendxnocndx  13426  plendxnocndx  13427  dsndxnplusgndx  13434  dsndxnmulrndx  13435  slotsdnscsi  13436  dsndxntsetndx  13437  slotsdifdsndx  13438  unifndxntsetndx  13444  slotsdifunifndx  13445  setsmsbasg  15344  setsmsdsg  15345