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

Theorem neeq12i 3035
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 2811 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 3021 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 198   = wceq 1653  wne 2969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2790  df-ne 2970
This theorem is referenced by:  3netr3g  3047  3netr4g  3048  oppchomfval  16684  oppcbas  16688  rescbas  16799  rescco  16802  rescabs  16803  odubas  17444  oppglem  18088  mgplem  18806  mgpress  18812  opprlem  18940  sralem  19496  srasca  19500  sravsca  19501  opsrbaslem  19796  zlmsca  20187  znbaslem  20204  thlbas  20361  thlle  20362  matsca  20542  tuslem  22395  setsmsbas  22604  setsmsds  22605  tngds  22776  ttgval  26103  ttglem  26104  cchhllem  26115  axlowdimlem6  26175  zlmds  30515  zlmtset  30516  nosepne  32335  hlhilslem  37950  zlmodzxzldeplem  43073
  Copyright terms: Public domain W3C validator