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

Theorem necon3bd 2483
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 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bd.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
31, 2syl5bi 208 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
43con1d 116 1  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  nelne1  2535  nelne2  2536  nssne1  3234  nssne2  3235  disjne  3500  difsn  3755  nbrne1  4040  nbrne2  4041  peano5  4679  oeeui  6600  domdifsn  6945  ac6sfi  7101  inf3lem2  7330  cnfcom3lem  7406  dfac9  7762  fin23lem21  7965  zneo  10094  modirr  11009  sqrmo  11737  pc2dvds  12931  pcadd  12937  4sqlem11  13002  latnlej  14174  sylow2blem3  14933  irredn0  15485  irredn1  15488  lssneln0  15709  lspsnne2  15871  lspfixed  15881  lspindpi  15885  lsmcv  15894  lspsolv  15896  isnzr2  16015  coe1tmmul  16353  dfac14  17312  fbdmn0  17529  filufint  17615  flimfnfcls  17723  alexsubALTlem2  17742  evth  18457  cphsqrcl2  18622  ovolicc2lem4  18879  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  deg1add  19489  abelthlem2  19808  logcnlem2  19990  angpined  20127  asinneg  20182  lgsne0  20572  lgsqr  20585  lgsquadlem2  20594  lgsquadlem3  20595  dvrunz  21100  spansncvi  22231  dmgmaddn0  23695  dedekindle  24083  axlowdimlem17  24586  broutsideof2  24745  dvreasin  24923  nninfnub  26461  pellexlem1  26914  dfac21  27164  pm13.14  27609  lsatcvatlem  29239  lkrlsp2  29293  opnlen0  29378  2llnne2N  29597  lnnat  29616  llnn0  29705  lplnn0N  29736  lplnllnneN  29745  llncvrlpln2  29746  llncvrlpln  29747  lvoln0N  29780  lplncvrlvol2  29804  lplncvrlvol  29805  dalempnes  29840  dalemqnet  29841  dalemcea  29849  dalem3  29853  cdlema1N  29980  cdlemb  29983  paddasslem5  30013  llnexchb2lem  30057  osumcllem4N  30148  pexmidlem1N  30159  lhp2lt  30190  lhp2atne  30223  lhp2at0ne  30225  4atexlemunv  30255  4atexlemex2  30260  trlne  30374  trlval4  30377  cdlemc4  30383  cdleme11dN  30451  cdleme11h  30455  cdlemednuN  30489  cdleme20j  30507  cdleme20k  30508  cdleme21at  30517  cdleme35f  30643  cdlemg11b  30831  dia2dimlem1  31254  dihmeetlem3N  31495  dihmeetlem15N  31511  dochsnnz  31640  dochexmidlem1  31650  dochexmidlem7  31656  mapdindp3  31912
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 177  df-ne 2448
  Copyright terms: Public domain W3C validator