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

Theorem necon2bd 2570
Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon2bd.1  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
Assertion
Ref Expression
necon2bd  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)

Proof of Theorem necon2bd
StepHypRef Expression
1 necon2bd.1 . . 3  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
2 df-ne 2523 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 217 . 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 1642    =/= wne 2521
This theorem is referenced by:  necon4d  2584  disjiun  4094  eceqoveq  6851  en3lp  7508  infpssrlem5  8023  nneo  10187  zeo2  10190  sqr2irr  12624  coprm  12876  dfphi2  12939  pltirr  14196  oddvdsnn0  14958  supnfcls  17817  flimfnfcls  17825  metds0  18457  metdseq0  18461  metnrmlem1a  18465  sineq0  19996  lgsqr  20697  staddi  22940  stadd3i  22942  erdszelem8  24133  ordcmp  25445  finminlem  25555  bezoutr1  26396  cvrnrefN  29541  trlnidatb  30435
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 2523
  Copyright terms: Public domain W3C validator