Theorem necon3ad 2613

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon3ad.1	|- ( ph -> ( ps -> A = B ) )

Assertion

Ref	Expression
necon3ad	|- ( ph -> ( A =/= B -> -. ps ) )

Proof of Theorem necon3ad

Step	Hyp	Ref	Expression
1		necon3ad.1	. 2 |- ( ph -> ( ps -> A = B ) )
2		id 22	. . 3 |- ( A =/= B -> A =/= B )
3	2	neneqd 2605	. 2 |- ( A =/= B -> -. A = B )
4	1, 3	nsyli 141	1 |- ( ph -> ( A =/= B -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1405   =/= wne 2598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-ne 2600

This theorem is referenced by:  necon1ad  2619  necon3d  2627  disjpss  3819  oeeulem  7286  enp1i  7788  canthp1lem2  9060  winalim2  9103  nlt1pi  9313  sqreulem  13339  rpnnen2lem11  14165  dvdseq  14240  eucalglt  14421  nprm  14438  pcprmpw2  14612  pcmpt  14618  expnprm  14628  prmlem0  14798  pltnle  15918  psgnunilem1  16840  pgpfi  16947  frgpnabllem1  17199  gsumval3a  17227  gsumval3aOLD  17228  ablfac1eulem  17441  pgpfaclem2  17451  lspdisjb  18090  lspdisj2  18091  obselocv  19055  0nnei  19904  t0dist  20117  t1sep  20162  ordthauslem  20175  hausflim  20772  bcthlem5  22057  bcth  22058  fta1g  22858  plyco0  22879  dgrnznn  22934  coeaddlem  22936  fta1  22994  vieta1lem2  22997  logcnlem3  23317  dvloglem  23321  dcubic  23500  mumullem2  23833  2sqlem8a  24025  dchrisum0flblem1  24072  colperpexlem2  24488  ocnel  26616  hatomistici  27680  sibfof  28774  outsideofrflx  30452  mblfinlem1  31403  cntotbnd  31554  heiborlem6  31574  lshpnel  31981  lshpcmp  31986  lfl1  32068  lkrshp  32103  lkrpssN  32161  atnlt  32311  atnle  32315  atlatmstc  32317  intnatN  32404  atbtwn  32443  llnnlt  32520  lplnnlt  32562  2llnjaN  32563  lvolnltN  32615  2lplnja  32616  dalem-cly  32668  dalem44  32713  2llnma3r  32785  cdlemblem  32790  lhpm0atN  33026  lhp2atnle  33030  cdlemednpq  33297  cdleme22cN  33341  cdlemg18b  33678  cdlemg42  33728  dia2dimlem1  34064  dochkrshp  34386  hgmapval0  34895  2f1fvneq  37921