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

Theorem necon3ad 2495
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 2463 . . 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 1632    =/= wne 2459
This theorem is referenced by:  necon3d  2497  disjpss  3518  oeeulem  6615  enp1i  7109  canthp1lem2  8291  winalim2  8334  nlt1pi  8546  sqreulem  11859  rpnnen2lem11  12519  dvdseq  12592  eucalglt  12771  nprm  12788  pcprmpw2  12950  pcmpt  12956  expnprm  12966  prmlem0  13123  pltnle  14116  pgpfi  14932  frgpnabllem1  15177  gsumval3a  15205  ablfac1eulem  15323  pgpfaclem2  15333  lspdisjb  15895  lspdisj2  15896  obselocv  16644  0nnei  16865  t0dist  17069  t1sep  17114  ordthauslem  17127  hausflim  17692  bcthlem5  18766  bcth  18767  fta1g  19569  plyco0  19590  coeaddlem  19646  fta1  19704  vieta1lem2  19707  logcnlem3  20007  dvloglem  20011  dcubic  20158  mumullem2  20434  2sqlem8a  20626  dchrisum0flblem1  20673  ocnel  21893  hatomistici  22958  outsideofrflx  24822  dmse1  25706  cntotbnd  26623  heiborlem6  26643  dgrnznn  27443  psgnunilem1  27519  lshpnel  29795  lshpcmp  29800  lfl1  29882  lkrshp  29917  lkrpssN  29975  atnlt  30125  atnle  30129  atlatmstc  30131  intnatN  30218  atbtwn  30257  llnnlt  30334  lplnnlt  30376  2llnjaN  30377  lvolnltN  30429  2lplnja  30430  dalem-cly  30482  dalem44  30527  2llnma3r  30599  cdlemblem  30604  lhpm0atN  30840  lhp2atnle  30844  cdlemednpq  31110  cdleme22cN  31153  cdlemg18b  31490  cdlemg42  31540  dia2dimlem1  31876  dochkrshp  32198  hgmapval0  32707
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 2461
  Copyright terms: Public domain W3C validator