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  13190  starvndxnplusgndx  13191  starvndxnmulrndx  13192  scandxnbasendx  13202  scandxnplusgndx  13203  scandxnmulrndx  13204  vscandxnbasendx  13207  vscandxnplusgndx  13208  vscandxnmulrndx  13209  vscandxnscandx  13210  ipndxnbasendx  13220  ipndxnplusgndx  13221  ipndxnmulrndx  13222  slotsdifipndx  13223  tsetndxnplusgndx  13240  tsetndxnmulrndx  13241  tsetndxnstarvndx  13242  slotstnscsi  13243  plendxnplusgndx  13254  plendxnmulrndx  13255  plendxnscandx  13256  plendxnvscandx  13257  slotsdifplendx  13258  basendxnocndx  13261  plendxnocndx  13262  dsndxnplusgndx  13269  dsndxnmulrndx  13270  slotsdnscsi  13271  dsndxntsetndx  13272  slotsdifdsndx  13273  unifndxntsetndx  13279  slotsdifunifndx  13280  setsmsbasg  15168  setsmsdsg  15169