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

Theorem neeq12i 2847
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 2623 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2833 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  3netr3g  2859  3netr4g  2860  oppchomfval  16146  oppcbas  16150  rescbas  16261  rescco  16264  rescabs  16265  odubas  16905  oppglem  17552  mgplem  18266  mgpress  18272  opprlem  18400  sralem  18947  srasca  18951  sravsca  18952  opsrbaslem  19247  opsrbaslemOLD  19248  zlmsca  19636  znbaslem  19653  znbaslemOLD  19654  thlbas  19807  thlle  19808  matsca  19988  tuslem  21829  setsmsbas  22038  setsmsds  22039  tngds  22210  ttgval  25501  ttglem  25502  cchhllem  25513  axlowdimlem6  25573  zlmds  29170  zlmtset  29171  hlhilslem  36072  zlmodzxzldeplem  42103
  Copyright terms: Public domain W3C validator