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

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

Proof of Theorem necon2ad
StepHypRef Expression
1 notnot1 122 . 2  |-  ( ps 
->  -.  -.  ps )
2 necon2ad.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
32necon3bd 2666 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  A  =/=  B ) )
41, 3syl5 32 1  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1398    =/= wne 2649
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 2651
This theorem is referenced by:  necon2d  2680  prneimg  4197  tz7.2  4852  nordeq  4886  omxpenlem  7611  pr2ne  8374  cflim2  8634  cfslb2n  8639  ltne  9670  sqrt2irr  14066  rpexp  14345  pcgcd1  14484  plttr  15799  odhash3  16795  lbspss  17923  nzrunit  18110  en2top  19654  fbfinnfr  20508  ufileu  20586  alexsubALTlem4  20716  lebnumlem1  21627  lebnumlem2  21628  lebnumlem3  21629  ivthlem2  22030  ivthlem3  22031  dvne0  22578  deg1nn0clb  22656  lgsmod  23794  axlowdimlem16  24462  normgt0  26242  nofulllem4  29705  lswn0  32607  dignn0flhalflem1  33490  islln2a  35638  islpln2a  35669  islvol2aN  35713  dalem1  35780  trlnidatb  36299
  Copyright terms: Public domain W3C validator