Theorem neeq12i 2848

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypotheses

Ref	Expression
neeq1i.1	⊢ 𝐴 = 𝐵
neeq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
neeq12i	⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Proof of Theorem neeq12i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
2		neeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
3	1, 2	eqeq12i 2624	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
4	3	necon3bii 2834	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Syntax hints:   ↔ wb 195   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  3netr3g  2860  3netr4g  2861  oppchomfval  16197  oppcbas  16201  rescbas  16312  rescco  16315  rescabs  16316  odubas  16956  oppglem  17603  mgplem  18317  mgpress  18323  opprlem  18451  sralem  18998  srasca  19002  sravsca  19003  opsrbaslem  19298  opsrbaslemOLD  19299  zlmsca  19688  znbaslem  19705  znbaslemOLD  19706  thlbas  19859  thlle  19860  matsca  20040  tuslem  21881  setsmsbas  22090  setsmsds  22091  tngds  22262  ttgval  25555  ttglem  25556  cchhllem  25567  axlowdimlem6  25627  zlmds  29336  zlmtset  29337  hlhilslem  36248  zlmodzxzldeplem  42081