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

Theorem neeq12i 2998
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 2774 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2984 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1632  wne 2932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933
This theorem is referenced by:  3netr3g  3010  3netr4g  3011  oppchomfval  16575  oppcbas  16579  rescbas  16690  rescco  16693  rescabs  16694  odubas  17334  oppglem  17980  mgplem  18694  mgpress  18700  opprlem  18828  sralem  19379  srasca  19383  sravsca  19384  opsrbaslem  19679  opsrbaslemOLD  19680  zlmsca  20071  znbaslem  20088  znbaslemOLD  20089  thlbas  20242  thlle  20243  matsca  20423  tuslem  22272  setsmsbas  22481  setsmsds  22482  tngds  22653  ttgval  25954  ttglem  25955  cchhllem  25966  axlowdimlem6  26026  zlmds  30317  zlmtset  30318  nosepne  32137  hlhilslem  37732  zlmodzxzldeplem  42797
  Copyright terms: Public domain W3C validator