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

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

Proof of Theorem necon3bd
StepHypRef Expression
1 nne 2575 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bd.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
31, 2syl5bi 209 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
43con1d 118 1  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2571
This theorem is referenced by:  nelne1  2660  nelne2  2661  nssne1  3368  nssne2  3369  disjne  3637  difsn  3897  nbrne1  4193  nbrne2  4194  peano5  4831  oeeui  6808  domdifsn  7154  ac6sfi  7314  inf3lem2  7544  cnfcom3lem  7620  dfac9  7976  fin23lem21  8179  zneo  10312  modirr  11245  sqrmo  12016  pc2dvds  13211  pcadd  13217  4sqlem11  13282  latnlej  14456  sylow2blem3  15215  irredn0  15767  irredn1  15770  lssneln0  15987  lspsnne2  16149  lspfixed  16159  lspindpi  16163  lsmcv  16172  lspsolv  16174  isnzr2  16293  coe1tmmul  16628  dfac14  17607  fbdmn0  17823  filufint  17909  flimfnfcls  18017  alexsubALTlem2  18036  evth  18941  cphsqrcl2  19106  ovolicc2lem4  19373  lhop1lem  19854  lhop1  19855  lhop2  19856  lhop  19857  deg1add  19983  abelthlem2  20305  logcnlem2  20491  angpined  20628  asinneg  20683  lgsne0  21074  lgsqr  21087  lgsquadlem2  21096  lgsquadlem3  21097  dvrunz  21978  spansncvi  23111  dmgmaddn0  24764  dedekindle  25145  axlowdimlem17  25805  broutsideof2  25964  dvreasin  26183  nninfnub  26349  pellexlem1  26786  dfac21  27036  pm13.14  27481  lsatcvatlem  29536  lkrlsp2  29590  opnlen0  29675  2llnne2N  29894  lnnat  29913  llnn0  30002  lplnn0N  30033  lplnllnneN  30042  llncvrlpln2  30043  llncvrlpln  30044  lvoln0N  30077  lplncvrlvol2  30101  lplncvrlvol  30102  dalempnes  30137  dalemqnet  30138  dalemcea  30146  dalem3  30150  cdlema1N  30277  cdlemb  30280  paddasslem5  30310  llnexchb2lem  30354  osumcllem4N  30445  pexmidlem1N  30456  lhp2lt  30487  lhp2atne  30520  lhp2at0ne  30522  4atexlemunv  30552  4atexlemex2  30557  trlne  30671  trlval4  30674  cdlemc4  30680  cdleme11dN  30748  cdleme11h  30752  cdlemednuN  30786  cdleme20j  30804  cdleme20k  30805  cdleme21at  30814  cdleme35f  30940  cdlemg11b  31128  dia2dimlem1  31551  dihmeetlem3N  31792  dihmeetlem15N  31808  dochsnnz  31937  dochexmidlem1  31947  dochexmidlem7  31953  mapdindp3  32209
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 178  df-ne 2573
  Copyright terms: Public domain W3C validator