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

Theorem neeq12i 3011
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 2997 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wne 2944
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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-ne 2945
This theorem is referenced by:  3netr3g  3023  3netr4g  3024  starvndxnbasendx  17186  starvndxnplusgndx  17187  starvndxnmulrndx  17188  scandxnbasendx  17198  scandxnplusgndx  17199  scandxnmulrndx  17200  vscandxnbasendx  17203  vscandxnplusgndx  17204  vscandxnmulrndx  17205  vscandxnscandx  17206  ipndxnbasendx  17214  ipndxnplusgndx  17215  ipndxnmulrndx  17216  slotsdifipndx  17217  tsetndxnplusgndx  17239  tsetndxnmulrndx  17240  tsetndxnstarvndx  17241  slotstnscsi  17242  plendxnplusgndx  17253  plendxnmulrndx  17254  plendxnscandx  17255  plendxnvscandx  17256  slotsdifplendx  17257  basendxnocndx  17265  plendxnocndx  17266  dsndxnplusgndx  17272  dsndxnmulrndx  17273  slotsdnscsi  17274  dsndxntsetndx  17275  slotsdifdsndx  17276  unifndxntsetndx  17282  slotsdifunifndx  17283  slotsdifplendx2  17299  slotsdifocndx  17300  oppchomfvalOLD  17596  oppcbasOLD  17601  rescbasOLD  17714  resccoOLD  17718  rescabsOLD  17720  odubasOLD  18182  oppglemOLD  19130  mgplemOLD  19902  mgpressOLD  19913  opprlemOLD  20056  sralemOLD  20642  srascaOLD  20650  sravscaOLD  20652  znbaslemOLD  20945  thlbasOLD  21104  thlleOLD  21106  opsrbaslemOLD  21454  matscaOLD  21766  tuslemOLD  23622  setsmsbasOLD  23832  setsmsdsOLD  23834  tngdsOLD  24015  nosepne  27031  lngndxnitvndx  27388  ttgvalOLD  27821  ttglemOLD  27823  cchhllemOLD  27839  axlowdimlem6  27899  zlmdsOLD  32547  zlmtsetOLD  32549  hlhilslemOLD  40405  oaomoencom  41654  zlmodzxzldeplem  46586  line2  46845  prstclevalOLD  47096  prstcocvalOLD  47099
  Copyright terms: Public domain W3C validator