Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq12i Structured version   Visualization version   GIF version

Theorem neeq12i 3086
 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
StepHypRef Expression
1 neeq1i.1 . . 3 𝐴 = 𝐵
2 neeq12i.2 . . 3 𝐶 = 𝐷
31, 2eqeq12i 2839 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 3072 1 (𝐴𝐶𝐵𝐷)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   = wceq 1530   ≠ wne 3020 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2116  ax-ext 2796 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2817  df-ne 3021 This theorem is referenced by:  3netr3g  3098  3netr4g  3099  oppchomfval  16976  oppcbas  16980  rescbas  17091  rescco  17094  rescabs  17095  odubas  17735  oppglem  18410  mgplem  19166  mgpress  19172  opprlem  19300  sralem  19871  srasca  19875  sravsca  19876  opsrbaslem  20178  zlmsca  20584  znbaslem  20601  thlbas  20756  thlle  20757  matsca  20940  tuslem  22791  setsmsbas  23000  setsmsds  23001  tngds  23172  ttgval  26576  ttglem  26577  cchhllem  26588  axlowdimlem6  26648  zlmds  31092  zlmtset  31093  nosepne  33070  hlhilslem  38942  zlmodzxzldeplem  44382  line2  44568
 Copyright terms: Public domain W3C validator