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

Theorem necon2ad 2494
Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon2ad.1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Assertion
Ref Expression
necon2ad  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )

Proof of Theorem necon2ad
StepHypRef Expression
1 nne 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon2ad.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
31, 2syl5bi 208 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  -.  ps )
)
43con4d 97 1  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon2d  2496  tz7.2  4377  nordeq  4411  omxpenlem  6963  pr2ne  7635  cflim2  7889  cfslb2n  7894  ltne  8917  sqr2irr  12527  rpexp  12799  pcgcd1  12929  plttr  14104  odhash3  14887  lbspss  15835  nzrunit  16018  en2top  16723  fbfinnfr  17536  ufileu  17614  alexsubALTlem4  17744  lebnumlem1  18459  lebnumlem2  18460  lebnumlem3  18461  ivthlem2  18812  ivthlem3  18813  dvne0  19358  deg1nn0clb  19476  lgsmod  20560  normgt0  21706  nofulllem4  24359  axlowdimlem16  24585  xrltneNEW  27657  prneimg  28073  islln2a  29706  islpln2a  29737  islvol2aN  29781  dalem1  29848  trlnidatb  30366
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 2448
  Copyright terms: Public domain W3C validator