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

Theorem necon3ad 2634
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 2602 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
31, 2syl6ibr 219 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =/=  B ) )
43con2d 109 1  |-  ( ph  ->  ( A  =/=  B  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon3d  2636  disjpss  3670  oeeulem  6836  enp1i  7335  canthp1lem2  8518  winalim2  8561  nlt1pi  8773  sqreulem  12153  rpnnen2lem11  12814  dvdseq  12887  eucalglt  13066  nprm  13083  pcprmpw2  13245  pcmpt  13251  expnprm  13261  prmlem0  13418  pltnle  14413  pgpfi  15229  frgpnabllem1  15474  gsumval3a  15502  ablfac1eulem  15620  pgpfaclem2  15630  lspdisjb  16188  lspdisj2  16189  obselocv  16945  0nnei  17166  t0dist  17379  t1sep  17424  ordthauslem  17437  hausflim  18003  bcthlem5  19271  bcth  19272  fta1g  20080  plyco0  20101  coeaddlem  20157  fta1  20215  vieta1lem2  20218  logcnlem3  20525  dvloglem  20529  dcubic  20676  mumullem2  20953  2sqlem8a  21145  dchrisum0flblem1  21192  ocnel  22790  hatomistici  23855  sibfof  24644  outsideofrflx  26026  mblfinlem  26207  cntotbnd  26459  heiborlem6  26479  dgrnznn  27272  psgnunilem1  27348  2f1fvneq  28027  lshpnel  29682  lshpcmp  29687  lfl1  29769  lkrshp  29804  lkrpssN  29862  atnlt  30012  atnle  30016  atlatmstc  30018  intnatN  30105  atbtwn  30144  llnnlt  30221  lplnnlt  30263  2llnjaN  30264  lvolnltN  30316  2lplnja  30317  dalem-cly  30369  dalem44  30414  2llnma3r  30486  cdlemblem  30491  lhpm0atN  30727  lhp2atnle  30731  cdlemednpq  30997  cdleme22cN  31040  cdlemg18b  31377  cdlemg42  31427  dia2dimlem1  31763  dochkrshp  32085  hgmapval0  32594
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 2600
  Copyright terms: Public domain W3C validator