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 1537   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

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

This theorem is referenced by:  3netr3g  3094  3netr4g  3095  oppchomfval  16984  oppcbas  16988  rescbas  17099  rescco  17102  rescabs  17103  odubas  17743  oppglem  18478  mgplem  19244  mgpress  19250  opprlem  19378  sralem  19949  srasca  19953  sravsca  19954  opsrbaslem  20258  zlmsca  20668  znbaslem  20685  thlbas  20840  thlle  20841  matsca  21024  tuslem  22876  setsmsbas  23085  setsmsds  23086  tngds  23257  ttgval  26661  ttglem  26662  cchhllem  26673  axlowdimlem6  26733  zlmds  31205  zlmtset  31206  nosepne  33185  hlhilslem  39089  zlmodzxzldeplem  44573  line2  44759