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

Theorem necon2ad 2654
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 2607 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon2ad.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
31, 2syl5bi 210 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  -.  ps )
)
43con4d 100 1  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon2d  2656  prneimg  3980  tz7.2  4568  nordeq  4602  omxpenlem  7211  pr2ne  7891  cflim2  8145  cfslb2n  8150  ltne  9172  sqr2irr  12850  rpexp  13122  pcgcd1  13252  plttr  14429  odhash3  15212  lbspss  16156  nzrunit  16339  en2top  17052  fbfinnfr  17875  ufileu  17953  alexsubALTlem4  18083  lebnumlem1  18988  lebnumlem2  18989  lebnumlem3  18990  ivthlem2  19351  ivthlem3  19352  dvne0  19897  deg1nn0clb  20015  lgsmod  21107  normgt0  22631  nofulllem4  25662  axlowdimlem16  25898  xrltneNEW  27635  lswrdn0  28282  islln2a  30376  islpln2a  30407  islvol2aN  30451  dalem1  30518  trlnidatb  31036
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator