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

Theorem necon3ad 2482
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
StepHypRef Expression
1 necon3ad.1 . . 3  |-  ( ph  ->  ( ps  ->  A  =  B ) )
2 nne 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
31, 2syl6ibr 218 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =/=  B ) )
43con2d 107 1  |-  ( ph  ->  ( A  =/=  B  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon3d  2484  disjpss  3505  oeeulem  6599  enp1i  7093  canthp1lem2  8275  winalim2  8318  nlt1pi  8530  sqreulem  11843  rpnnen2lem11  12503  dvdseq  12576  eucalglt  12755  nprm  12772  pcprmpw2  12934  pcmpt  12940  expnprm  12950  prmlem0  13107  pltnle  14100  pgpfi  14916  frgpnabllem1  15161  gsumval3a  15189  ablfac1eulem  15307  pgpfaclem2  15317  lspdisjb  15879  lspdisj2  15880  obselocv  16628  0nnei  16849  t0dist  17053  t1sep  17098  ordthauslem  17111  hausflim  17676  bcthlem5  18750  bcth  18751  fta1g  19553  plyco0  19574  coeaddlem  19630  fta1  19688  vieta1lem2  19691  logcnlem3  19991  dvloglem  19995  dcubic  20142  mumullem2  20418  2sqlem8a  20610  dchrisum0flblem1  20657  ocnel  21877  hatomistici  22942  outsideofrflx  24750  dmse1  25603  cntotbnd  26520  heiborlem6  26540  dgrnznn  27340  psgnunilem1  27416  lshpnel  29173  lshpcmp  29178  lfl1  29260  lkrshp  29295  lkrpssN  29353  atnlt  29503  atnle  29507  atlatmstc  29509  intnatN  29596  atbtwn  29635  llnnlt  29712  lplnnlt  29754  2llnjaN  29755  lvolnltN  29807  2lplnja  29808  dalem-cly  29860  dalem44  29905  2llnma3r  29977  cdlemblem  29982  lhpm0atN  30218  lhp2atnle  30222  cdlemednpq  30488  cdleme22cN  30531  cdlemg18b  30868  cdlemg42  30918  dia2dimlem1  31254  dochkrshp  31576  hgmapval0  32085
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 177  df-ne 2448
  Copyright terms: Public domain W3C validator