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

Theorem necon1bd 2666
Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon1bd.1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Assertion
Ref Expression
necon1bd  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )

Proof of Theorem necon1bd
StepHypRef Expression
1 necon1bd.1 . . 3  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
21con3d 127 . 2  |-  ( ph  ->  ( -.  ps  ->  -.  A  =/=  B ) )
3 nne 2602 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 218 1  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  suppssr  5856  fvclss  5972  eceqoveq  7001  fofinf1o  7379  cantnfp1lem3  7628  cantnfp1  7629  mul0or  9654  inelr  9982  rimul  9983  rlimuni  12336  pc2dvds  13244  divsfval  13764  pleval2i  14413  lssvs0or  16174  lspsnat  16209  lmmo  17436  filssufilg  17935  hausflimi  18004  fclscf  18049  xrsmopn  18835  rectbntr0  18855  bcth3  19276  limcco  19772  ig1pdvds  20091  plyco0  20103  plypf1  20123  coeeulem  20135  coeidlem  20148  coeid3  20151  coemullem  20160  coemulhi  20164  coemulc  20165  dgradd2  20178  vieta1lem2  20220  dvtaylp  20278  musum  20968  perfectlem2  21006  dchrelbas3  21014  dchrmulid2  21028  dchreq  21034  dchrsum  21045  dchrisum0re  21199  elspansn5  23068  atomli  23877  onsucconi  26179  congabseq  27030  lshpcmp  29723  lsator0sp  29736  atnle  30052  atlatmstc  30054  osumcllem8N  30697  osumcllem11N  30700  pexmidlem5N  30708  pexmidlem8N  30711  dochsat0  32192  dochexmidlem5  32199  dochexmidlem8  32202
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