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

Theorem necon2bd 2664
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 2647 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 226 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =  B )
)
43con2d 115 1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2647
This theorem is referenced by:  necon4bd  2671  necon4d  2676  disjiun  4385  eceqoveq  7310  en3lp  7928  infpssrlem5  8582  nneo  10831  zeo2  10834  sqr2irr  13644  coprm  13899  dfphi2  13962  pltirr  15247  oddvdsnn0  16163  psgnodpmr  18140  supnfcls  19720  flimfnfcls  19728  metds0  20553  metdseq0  20557  metnrmlem1a  20561  sineq0  22111  lgsqr  22813  staddi  25797  stadd3i  25799  eulerpartlems  26882  erdszelem8  27225  ordcmp  28432  finminlem  28656  bezoutr1  29472  cvrnrefN  33246  trlnidatb  34140
  Copyright terms: Public domain W3C validator