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  13170  starvndxnplusgndx  13171  starvndxnmulrndx  13172  scandxnbasendx  13182  scandxnplusgndx  13183  scandxnmulrndx  13184  vscandxnbasendx  13187  vscandxnplusgndx  13188  vscandxnmulrndx  13189  vscandxnscandx  13190  ipndxnbasendx  13200  ipndxnplusgndx  13201  ipndxnmulrndx  13202  slotsdifipndx  13203  tsetndxnplusgndx  13220  tsetndxnmulrndx  13221  tsetndxnstarvndx  13222  slotstnscsi  13223  plendxnplusgndx  13234  plendxnmulrndx  13235  plendxnscandx  13236  plendxnvscandx  13237  slotsdifplendx  13238  basendxnocndx  13241  plendxnocndx  13242  dsndxnplusgndx  13249  dsndxnmulrndx  13250  slotsdnscsi  13251  dsndxntsetndx  13252  slotsdifdsndx  13253  unifndxntsetndx  13259  slotsdifunifndx  13260  setsmsbasg  15147  setsmsdsg  15148