Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq12d Unicode version

Theorem neeq12d 2736
 Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
neeq1d.1
neeq12d.2
Assertion
Ref Expression
neeq12d

Proof of Theorem neeq12d
StepHypRef Expression
1 neeq1d.1 . . 3
2 neeq12d.2 . . 3
31, 2eqeq12d 2479 . 2
43necon3bid 2715 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  =/=wne 2652 This theorem is referenced by:  3netr3dOLD  2761  3netr4dOLD  2763  fnelnfp  6101  suppval  6920  infpssrlem4  8707  injresinjlem  11925  sgrp2nmndlem5  16047  pmtr3ncom  16500  isnzr  17907  ptcmplem2  20553  iscgra  24169  axlowdimlem6  24250  axlowdimlem14  24258  usgrcyclnl1  24640  constr3lem6  24649  4cycl4dv4e  24668  usg2wotspth  24884  2spontn0vne  24887  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  numclwwlk5  25112  signsvvfval  28535  signsvfn  28539  derangsn  28614  derangenlem  28615  subfacp1lem3  28626  subfacp1lem5  28628  subfacp1lem6  28629  subfacp1  28630  sltval2  29416  sltres  29424  nodenselem3  29443  nodenselem5  29445  nodenselem7  29447  nofulllem4  29465  nofulllem5  29466  fvtransport  29682  stoweidlem43  31825  nnsgrpnmnd  32506  2zrngnmlid  32755  pgrpgt2nabl  32959  ldepsnlinc  33109  bnj1534  33911  bnj1542  33915  bnj1280  34076  cdlemkid3N  36659  cdlemkid4  36660 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-ne 2654
 Copyright terms: Public domain W3C validator