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

Theorem necon3bd 2640
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 2607 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bd.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
31, 2syl5bi 210 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
43con1d 119 1  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  nelne1  2695  nelne2  2696  nssne1  3406  nssne2  3407  disjne  3675  difsn  3935  nbrne1  4232  nbrne2  4233  peano5  4871  oeeui  6848  domdifsn  7194  ac6sfi  7354  inf3lem2  7587  cnfcom3lem  7663  dfac9  8021  fin23lem21  8224  zneo  10357  modirr  11291  sqrmo  12062  pc2dvds  13257  pcadd  13263  4sqlem11  13328  latnlej  14502  sylow2blem3  15261  irredn0  15813  irredn1  15816  lssneln0  16033  lspsnne2  16195  lspfixed  16205  lspindpi  16209  lsmcv  16218  lspsolv  16220  isnzr2  16339  coe1tmmul  16674  dfac14  17655  fbdmn0  17871  filufint  17957  flimfnfcls  18065  alexsubALTlem2  18084  evth  18989  cphsqrcl2  19154  ovolicc2lem4  19421  lhop1lem  19902  lhop1  19903  lhop2  19904  lhop  19905  deg1add  20031  abelthlem2  20353  logcnlem2  20539  angpined  20676  asinneg  20731  lgsne0  21122  lgsqr  21135  lgsquadlem2  21144  lgsquadlem3  21145  dvrunz  22026  spansncvi  23159  dmgmaddn0  24812  dedekindle  25193  axlowdimlem17  25902  broutsideof2  26061  dvreasin  26304  nninfnub  26469  pellexlem1  26906  dfac21  27155  pm13.14  27600  lsatcvatlem  29921  lkrlsp2  29975  opnlen0  30060  2llnne2N  30279  lnnat  30298  llnn0  30387  lplnn0N  30418  lplnllnneN  30427  llncvrlpln2  30428  llncvrlpln  30429  lvoln0N  30462  lplncvrlvol2  30486  lplncvrlvol  30487  dalempnes  30522  dalemqnet  30523  dalemcea  30531  dalem3  30535  cdlema1N  30662  cdlemb  30665  paddasslem5  30695  llnexchb2lem  30739  osumcllem4N  30830  pexmidlem1N  30841  lhp2lt  30872  lhp2atne  30905  lhp2at0ne  30907  4atexlemunv  30937  4atexlemex2  30942  trlne  31056  trlval4  31059  cdlemc4  31065  cdleme11dN  31133  cdleme11h  31137  cdlemednuN  31171  cdleme20j  31189  cdleme20k  31190  cdleme21at  31199  cdleme35f  31325  cdlemg11b  31513  dia2dimlem1  31936  dihmeetlem3N  32177  dihmeetlem15N  32193  dochsnnz  32322  dochexmidlem1  32332  dochexmidlem7  32338  mapdindp3  32594
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator