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

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3
2		neeq12d.2	. . 3
3	1, 2	eqeq12d 2479	. 2
4	3	necon3bid 2715	1

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