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

Theorem neeq12i 3009
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 2785 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2995 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631  wne 2943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-ne 2944
This theorem is referenced by:  3netr3g  3021  3netr4g  3022  oppchomfval  16581  oppcbas  16585  rescbas  16696  rescco  16699  rescabs  16700  odubas  17341  oppglem  17987  mgplem  18702  mgpress  18708  opprlem  18836  sralem  19392  srasca  19396  sravsca  19397  opsrbaslem  19692  opsrbaslemOLD  19693  zlmsca  20084  znbaslem  20101  znbaslemOLD  20102  thlbas  20257  thlle  20258  matsca  20438  tuslem  22291  setsmsbas  22500  setsmsds  22501  tngds  22672  ttgval  25976  ttglem  25977  cchhllem  25988  axlowdimlem6  26048  zlmds  30348  zlmtset  30349  nosepne  32168  hlhilslem  37748  zlmodzxzldeplem  42815
  Copyright terms: Public domain W3C validator