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

Theorem necon2ad 2665
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 2664 . 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 1370    =/= wne 2648
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 2650
This theorem is referenced by:  necon2d  2678  prneimg  4162  tz7.2  4813  nordeq  4847  omxpenlem  7523  pr2ne  8284  cflim2  8544  cfslb2n  8549  ltne  9583  sqr2irr  13650  rpexp  13925  pcgcd1  14062  plttr  15260  odhash3  16197  lbspss  17287  nzrunit  17472  en2top  18723  fbfinnfr  19547  ufileu  19625  alexsubALTlem4  19755  lebnumlem1  20666  lebnumlem2  20667  lebnumlem3  20668  ivthlem2  21069  ivthlem3  21070  dvne0  21617  deg1nn0clb  21695  lgsmod  22794  axlowdimlem16  23356  normgt0  24682  nofulllem4  27991  lswn0  30407  islln2a  33500  islpln2a  33531  islvol2aN  33575  dalem1  33642  trlnidatb  34160
  Copyright terms: Public domain W3C validator