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

Theorem neeq12i 3007
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 2755 . 2 (𝐴 = 𝐶𝐵 = 𝐷)
43necon3bii 2993 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  3netr3g  3019  3netr4g  3020  starvndxnbasendx  17348  starvndxnplusgndx  17349  starvndxnmulrndx  17350  scandxnbasendx  17360  scandxnplusgndx  17361  scandxnmulrndx  17362  vscandxnbasendx  17365  vscandxnplusgndx  17366  vscandxnmulrndx  17367  vscandxnscandx  17368  ipndxnbasendx  17376  ipndxnplusgndx  17377  ipndxnmulrndx  17378  slotsdifipndx  17379  tsetndxnplusgndx  17401  tsetndxnmulrndx  17402  tsetndxnstarvndx  17403  slotstnscsi  17404  plendxnplusgndx  17415  plendxnmulrndx  17416  plendxnscandx  17417  plendxnvscandx  17418  slotsdifplendx  17419  basendxnocndx  17427  plendxnocndx  17428  dsndxnplusgndx  17434  dsndxnmulrndx  17435  slotsdnscsi  17436  dsndxntsetndx  17437  slotsdifdsndx  17438  unifndxntsetndx  17444  slotsdifunifndx  17445  slotsdifplendx2  17461  slotsdifocndx  17462  rescabsOLD  17878  odubasOLD  18337  oppglemOLD  19369  opprlemOLD  20340  sralemOLD  21176  srascaOLD  21184  sravscaOLD  21186  znbaslemOLD  21554  thlbasOLD  21715  thlleOLD  21717  opsrbaslemOLD  22068  matscaOLD  22420  tuslemOLD  24276  setsmsbasOLD  24486  setsmsdsOLD  24488  tngdsOLD  24669  nosepne  27725  lngndxnitvndx  28451  ttgvalOLD  28884  ttglemOLD  28886  cchhllemOLD  28902  axlowdimlem6  28962  zlmdsOLD  33962  zlmtsetOLD  33964  hlhilslemOLD  41941  oaomoencom  43330  zlmodzxzldeplem  48415  line2  48673  prstclevalOLD  49158  prstcocvalOLD  49161
  Copyright terms: Public domain W3C validator