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

Theorem necon3bd 2666
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 2655 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bd.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
31, 2syl5bi 217 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
43con1d 124 1  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1398    =/= wne 2649
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 2651
This theorem is referenced by:  necon2ad  2667  nelne1  2783  nelne2  2784  nssne1  3545  nssne2  3546  disjne  3860  difsn  4150  nbrne1  4456  nbrne2  4457  peano5  6696  oeeui  7243  domdifsn  7593  ac6sfi  7756  inf3lem2  8037  cnfcom3lem  8138  cnfcom3lemOLD  8146  dfac9  8507  fin23lem21  8710  dedekindle  9734  zneo  10941  modirr  12042  sqrmo  13170  pc2dvds  14489  pcadd  14495  4sqlem11  14560  latnlej  15900  sylow2blem3  16844  irredn0  17550  irredn1  17553  lssneln0  17796  lspsnne2  17962  lspfixed  17972  lspindpi  17976  lsmcv  17985  lspsolv  17987  isnzr2  18109  coe1tmmul  18516  dfac14  20288  fbdmn0  20504  filufint  20590  flimfnfcls  20698  alexsubALTlem2  20717  evth  21628  cphsqrtcl2  21802  ovolicc2lem4  22100  lhop1lem  22583  lhop1  22584  lhop2  22585  lhop  22586  deg1add  22673  abelthlem2  22996  logcnlem2  23195  angpined  23361  asinneg  23417  lgsne0  23809  lgsqr  23822  lgsquadlem2  23831  lgsquadlem3  23832  axlowdimlem17  24466  dvrunz  25636  spansncvi  26771  dmgmaddn0  28832  broutsideof2  30003  dvasin  30346  dvacos  30347  nninfnub  30487  pellexlem1  31007  dfac21  31254  pm13.14  31560  uzlidlring  33008  suppdm  33385  lsatcvatlem  35190  lkrlsp2  35244  opnlen0  35329  2llnne2N  35548  lnnat  35567  llnn0  35656  lplnn0N  35687  lplnllnneN  35696  llncvrlpln2  35697  llncvrlpln  35698  lvoln0N  35731  lplncvrlvol2  35755  lplncvrlvol  35756  dalempnes  35791  dalemqnet  35792  dalemcea  35800  dalem3  35804  cdlema1N  35931  cdlemb  35934  paddasslem5  35964  llnexchb2lem  36008  osumcllem4N  36099  pexmidlem1N  36110  lhp2lt  36141  lhp2atne  36174  lhp2at0ne  36176  4atexlemunv  36206  4atexlemex2  36211  trlne  36326  trlval4  36329  cdlemc4  36335  cdleme11dN  36403  cdleme11h  36407  cdlemednuN  36441  cdleme20j  36460  cdleme20k  36461  cdleme21at  36470  cdleme35f  36596  cdlemg11b  36784  dia2dimlem1  37207  dihmeetlem3N  37448  dihmeetlem15N  37464  dochsnnz  37593  dochexmidlem1  37603  dochexmidlem7  37609  mapdindp3  37865
  Copyright terms: Public domain W3C validator