Theorem neeq12i 3082

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

Syntax hints:   ↔ wb 208   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  3netr3g  3094  3netr4g  3095  oppchomfval  16978  oppcbas  16982  rescbas  17093  rescco  17096  rescabs  17097  odubas  17737  oppglem  18472  mgplem  19238  mgpress  19244  opprlem  19372  sralem  19943  srasca  19947  sravsca  19948  opsrbaslem  20252  zlmsca  20662  znbaslem  20679  thlbas  20834  thlle  20835  matsca  21018  tuslem  22870  setsmsbas  23079  setsmsds  23080  tngds  23251  ttgval  26655  ttglem  26656  cchhllem  26667  axlowdimlem6  26727  zlmds  31200  zlmtset  31201  nosepne  33180  hlhilslem  39068  zlmodzxzldeplem  44546  line2  44732