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

Theorem necon2ad 2680
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 2679 . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon2d  2693  prneimg  4207  tz7.2  4863  nordeq  4897  omxpenlem  7619  pr2ne  8384  cflim2  8644  cfslb2n  8649  ltne  9682  sqrt2irr  13846  rpexp  14123  pcgcd1  14262  plttr  15460  odhash3  16411  lbspss  17540  nzrunit  17726  en2top  19293  fbfinnfr  20169  ufileu  20247  alexsubALTlem4  20377  lebnumlem1  21288  lebnumlem2  21289  lebnumlem3  21290  ivthlem2  21691  ivthlem3  21692  dvne0  22239  deg1nn0clb  22317  lgsmod  23421  axlowdimlem16  24033  normgt0  25817  nofulllem4  29318  lswn0  32037  islln2a  34530  islpln2a  34561  islvol2aN  34605  dalem1  34672  trlnidatb  35190
  Copyright terms: Public domain W3C validator