Theorem neeq12i 3035

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 2811	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)
4	3	necon3bii 3021	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)

Syntax hints:   ↔ wb 198   = wceq 1653   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2790  df-ne 2970

This theorem is referenced by:  3netr3g  3047  3netr4g  3048  oppchomfval  16684  oppcbas  16688  rescbas  16799  rescco  16802  rescabs  16803  odubas  17444  oppglem  18088  mgplem  18806  mgpress  18812  opprlem  18940  sralem  19496  srasca  19500  sravsca  19501  opsrbaslem  19796  zlmsca  20187  znbaslem  20204  thlbas  20361  thlle  20362  matsca  20542  tuslem  22395  setsmsbas  22604  setsmsds  22605  tngds  22776  ttgval  26103  ttglem  26104  cchhllem  26115  axlowdimlem6  26175  zlmds  30515  zlmtset  30516  nosepne  32335  hlhilslem  37950  zlmodzxzldeplem  43073