Theorem necon3ad 2603

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 2571	. . 3 |- ( -. A =/= B <-> A = B )
3	1, 2	syl6ibr 219	. 2 |- ( ph -> ( ps -> -. A =/= B ) )
4	3	con2d 109	1 |- ( ph -> ( A =/= B -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1649   =/= wne 2567

This theorem is referenced by:  necon3d  2605  disjpss  3638  oeeulem  6803  enp1i  7302  canthp1lem2  8484  winalim2  8527  nlt1pi  8739  sqreulem  12118  rpnnen2lem11  12779  dvdseq  12852  eucalglt  13031  nprm  13048  pcprmpw2  13210  pcmpt  13216  expnprm  13226  prmlem0  13383  pltnle  14378  pgpfi  15194  frgpnabllem1  15439  gsumval3a  15467  ablfac1eulem  15585  pgpfaclem2  15595  lspdisjb  16153  lspdisj2  16154  obselocv  16910  0nnei  17131  t0dist  17343  t1sep  17388  ordthauslem  17401  hausflim  17966  bcthlem5  19234  bcth  19235  fta1g  20043  plyco0  20064  coeaddlem  20120  fta1  20178  vieta1lem2  20181  logcnlem3  20488  dvloglem  20492  dcubic  20639  mumullem2  20916  2sqlem8a  21108  dchrisum0flblem1  21155  ocnel  22753  hatomistici  23818  sibfof  24607  outsideofrflx  25965  mblfinlem  26143  cntotbnd  26395  heiborlem6  26415  dgrnznn  27208  psgnunilem1  27284  2f1fvneq  27958  lshpnel  29466  lshpcmp  29471  lfl1  29553  lkrshp  29588  lkrpssN  29646  atnlt  29796  atnle  29800  atlatmstc  29802  intnatN  29889  atbtwn  29928  llnnlt  30005  lplnnlt  30047  2llnjaN  30048  lvolnltN  30100  2lplnja  30101  dalem-cly  30153  dalem44  30198  2llnma3r  30270  cdlemblem  30275  lhpm0atN  30511  lhp2atnle  30515  cdlemednpq  30781  cdleme22cN  30824  cdlemg18b  31161  cdlemg42  31211  dia2dimlem1  31547  dochkrshp  31869  hgmapval0  32378

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

This theorem depends on definitions:  df-bi 178  df-ne 2569