Theorem necon3ad 2639

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

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	. . 3 |- ( ph -> ( ps -> A = B ) )
2		nne 2607	. . 3 |- ( -. A =/= B <-> A = B )
3	1, 2	syl6ibr 227	. 2 |- ( ph -> ( ps -> -. A =/= B ) )
4	3	con2d 115	1 |- ( ph -> ( A =/= B -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1369   =/= wne 2601

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 2603

This theorem is referenced by:  necon3d  2641  disjpss  3724  oeeulem  7032  enp1i  7539  canthp1lem2  8812  winalim2  8855  nlt1pi  9067  sqreulem  12839  rpnnen2lem11  13499  dvdseq  13572  eucalglt  13752  nprm  13769  pcprmpw2  13940  pcmpt  13946  expnprm  13956  prmlem0  14125  pltnle  15128  psgnunilem1  15990  pgpfi  16095  frgpnabllem1  16342  gsumval3a  16370  gsumval3aOLD  16371  ablfac1eulem  16561  pgpfaclem2  16571  lspdisjb  17184  lspdisj2  17185  obselocv  18128  0nnei  18691  t0dist  18904  t1sep  18949  ordthauslem  18962  hausflim  19529  bcthlem5  20814  bcth  20815  fta1g  21614  plyco0  21635  coeaddlem  21691  fta1  21749  vieta1lem2  21752  logcnlem3  22064  dvloglem  22068  dcubic  22216  mumullem2  22493  2sqlem8a  22685  dchrisum0flblem1  22732  ocnel  24652  hatomistici  25717  sibfof  26678  outsideofrflx  28109  mblfinlem1  28381  cntotbnd  28648  heiborlem6  28668  dgrnznn  29445  2f1fvneq  30096  lshpnel  32468  lshpcmp  32473  lfl1  32555  lkrshp  32590  lkrpssN  32648  atnlt  32798  atnle  32802  atlatmstc  32804  intnatN  32891  atbtwn  32930  llnnlt  33007  lplnnlt  33049  2llnjaN  33050  lvolnltN  33102  2lplnja  33103  dalem-cly  33155  dalem44  33200  2llnma3r  33272  cdlemblem  33277  lhpm0atN  33513  lhp2atnle  33517  cdlemednpq  33783  cdleme22cN  33826  cdlemg18b  34163  cdlemg42  34213  dia2dimlem1  34549  dochkrshp  34871  hgmapval0  35380