Theorem neeq12i 2417

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

Syntax hints:   ↔ wb 105   = wceq 1395   ≠ wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  3netr3g  2434  3netr4g  2435  starvndxnbasendx  13215  starvndxnplusgndx  13216  starvndxnmulrndx  13217  scandxnbasendx  13227  scandxnplusgndx  13228  scandxnmulrndx  13229  vscandxnbasendx  13232  vscandxnplusgndx  13233  vscandxnmulrndx  13234  vscandxnscandx  13235  ipndxnbasendx  13245  ipndxnplusgndx  13246  ipndxnmulrndx  13247  slotsdifipndx  13248  tsetndxnplusgndx  13265  tsetndxnmulrndx  13266  tsetndxnstarvndx  13267  slotstnscsi  13268  plendxnplusgndx  13279  plendxnmulrndx  13280  plendxnscandx  13281  plendxnvscandx  13282  slotsdifplendx  13283  basendxnocndx  13286  plendxnocndx  13287  dsndxnplusgndx  13294  dsndxnmulrndx  13295  slotsdnscsi  13296  dsndxntsetndx  13297  slotsdifdsndx  13298  unifndxntsetndx  13304  slotsdifunifndx  13305  setsmsbasg  15193  setsmsdsg  15194