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

Theorem necon3bd 2604
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 2571 . . 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 2567
This theorem is referenced by:  nelne1  2656  nelne2  2657  nssne1  3364  nssne2  3365  disjne  3633  difsn  3893  nbrne1  4189  nbrne2  4190  peano5  4827  oeeui  6804  domdifsn  7150  ac6sfi  7310  inf3lem2  7540  cnfcom3lem  7616  dfac9  7972  fin23lem21  8175  zneo  10308  modirr  11241  sqrmo  12012  pc2dvds  13207  pcadd  13213  4sqlem11  13278  latnlej  14452  sylow2blem3  15211  irredn0  15763  irredn1  15766  lssneln0  15983  lspsnne2  16145  lspfixed  16155  lspindpi  16159  lsmcv  16168  lspsolv  16170  isnzr2  16289  coe1tmmul  16624  dfac14  17603  fbdmn0  17819  filufint  17905  flimfnfcls  18013  alexsubALTlem2  18032  evth  18937  cphsqrcl2  19102  ovolicc2lem4  19369  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  deg1add  19979  abelthlem2  20301  logcnlem2  20487  angpined  20624  asinneg  20679  lgsne0  21070  lgsqr  21083  lgsquadlem2  21092  lgsquadlem3  21093  dvrunz  21974  spansncvi  23107  dmgmaddn0  24760  dedekindle  25141  axlowdimlem17  25801  broutsideof2  25960  dvreasin  26179  nninfnub  26345  pellexlem1  26782  dfac21  27032  pm13.14  27477  lsatcvatlem  29532  lkrlsp2  29586  opnlen0  29671  2llnne2N  29890  lnnat  29909  llnn0  29998  lplnn0N  30029  lplnllnneN  30038  llncvrlpln2  30039  llncvrlpln  30040  lvoln0N  30073  lplncvrlvol2  30097  lplncvrlvol  30098  dalempnes  30133  dalemqnet  30134  dalemcea  30142  dalem3  30146  cdlema1N  30273  cdlemb  30276  paddasslem5  30306  llnexchb2lem  30350  osumcllem4N  30441  pexmidlem1N  30452  lhp2lt  30483  lhp2atne  30516  lhp2at0ne  30518  4atexlemunv  30548  4atexlemex2  30553  trlne  30667  trlval4  30670  cdlemc4  30676  cdleme11dN  30744  cdleme11h  30748  cdlemednuN  30782  cdleme20j  30800  cdleme20k  30801  cdleme21at  30810  cdleme35f  30936  cdlemg11b  31124  dia2dimlem1  31547  dihmeetlem3N  31788  dihmeetlem15N  31804  dochsnnz  31933  dochexmidlem1  31943  dochexmidlem7  31949  mapdindp3  32205
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 2569
  Copyright terms: Public domain W3C validator