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

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
StepHypRef Expression
1 neeq1i.1 . . 3 𝐴 = 𝐵
2 neeq12i.2 . . 3 𝐶 = 𝐷
31, 2eqeq12i 2836 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 3068 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  3netr3g  3094  3netr4g  3095  oppchomfval  16974  oppcbas  16978  rescbas  17089  rescco  17092  rescabs  17093  odubas  17733  oppglem  18418  mgplem  19175  mgpress  19181  opprlem  19309  sralem  19880  srasca  19884  sravsca  19885  opsrbaslem  20188  zlmsca  20598  znbaslem  20615  thlbas  20770  thlle  20771  matsca  20954  tuslem  22805  setsmsbas  23014  setsmsds  23015  tngds  23186  ttgval  26589  ttglem  26590  cchhllem  26601  axlowdimlem6  26661  zlmds  31105  zlmtset  31106  nosepne  33083  hlhilslem  38956  zlmodzxzldeplem  44451  line2  44637
  Copyright terms: Public domain W3C validator