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

Theorem neeq12i 3010
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 2756 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2996 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1539  wne 2943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944
This theorem is referenced by:  3netr3g  3022  3netr4g  3023  starvndxnbasendx  17014  starvndxnplusgndx  17015  starvndxnmulrndx  17016  scandxnbasendx  17026  scandxnplusgndx  17027  scandxnmulrndx  17028  vscandxnbasendx  17031  vscandxnplusgndx  17032  vscandxnmulrndx  17033  vscandxnscandx  17034  ipndxnbasendx  17042  ipndxnplusgndx  17043  ipndxnmulrndx  17044  slotsdifipndx  17045  tsetndxnplusgndx  17067  tsetndxnmulrndx  17068  tsetndxnstarvndx  17069  slotstnscsi  17070  plendxnplusgndx  17081  plendxnmulrndx  17082  plendxnscandx  17083  plendxnvscandx  17084  slotsdifplendx  17085  basendxnocndx  17093  plendxnocndx  17094  dsndxnplusgndx  17100  dsndxnmulrndx  17101  slotsdnscsi  17102  dsndxntsetndx  17103  slotsdifdsndx  17104  unifndxntsetndx  17110  slotsdifunifndx  17111  slotsdifplendx2  17127  slotsdifocndx  17128  oppchomfvalOLD  17424  oppcbasOLD  17429  rescbasOLD  17542  resccoOLD  17546  rescabsOLD  17548  odubasOLD  18010  oppglemOLD  18955  mgplemOLD  19725  mgpressOLD  19736  opprlemOLD  19868  sralemOLD  20440  srascaOLD  20448  sravscaOLD  20450  znbaslemOLD  20743  thlbasOLD  20902  thlleOLD  20904  opsrbaslemOLD  21251  matscaOLD  21563  tuslemOLD  23419  setsmsbasOLD  23629  setsmsdsOLD  23631  tngdsOLD  23812  lngndxnitvndx  26804  ttgvalOLD  27237  ttglemOLD  27239  cchhllemOLD  27255  axlowdimlem6  27315  zlmdsOLD  31913  zlmtsetOLD  31915  nosepne  33883  hlhilslemOLD  39953  zlmodzxzldeplem  45839  line2  46098  prstclevalOLD  46350  prstcocvalOLD  46353
  Copyright terms: Public domain W3C validator