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

Theorem necon3bd 2485
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 2452 . . 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 1625    =/= wne 2448
This theorem is referenced by:  nelne1  2537  nelne2  2538  nssne1  3236  nssne2  3237  disjne  3502  difsn  3757  nbrne1  4042  nbrne2  4043  peano5  4681  oeeui  6602  domdifsn  6947  ac6sfi  7103  inf3lem2  7332  cnfcom3lem  7408  dfac9  7764  fin23lem21  7967  zneo  10096  modirr  11011  sqrmo  11739  pc2dvds  12933  pcadd  12939  4sqlem11  13004  latnlej  14176  sylow2blem3  14935  irredn0  15487  irredn1  15490  lssneln0  15711  lspsnne2  15873  lspfixed  15883  lspindpi  15887  lsmcv  15896  lspsolv  15898  isnzr2  16017  coe1tmmul  16355  dfac14  17314  fbdmn0  17531  filufint  17617  flimfnfcls  17725  alexsubALTlem2  17744  evth  18459  cphsqrcl2  18624  ovolicc2lem4  18881  lhop1lem  19362  lhop1  19363  lhop2  19364  lhop  19365  deg1add  19491  abelthlem2  19810  logcnlem2  19992  angpined  20129  asinneg  20184  lgsne0  20574  lgsqr  20587  lgsquadlem2  20596  lgsquadlem3  20597  dvrunz  21102  spansncvi  22233  dmgmaddn0  23697  dedekindle  24085  axlowdimlem17  24588  broutsideof2  24747  dvreasin  24925  nninfnub  26472  pellexlem1  26925  dfac21  27175  pm13.14  27620  lsatcvatlem  29312  lkrlsp2  29366  opnlen0  29451  2llnne2N  29670  lnnat  29689  llnn0  29778  lplnn0N  29809  lplnllnneN  29818  llncvrlpln2  29819  llncvrlpln  29820  lvoln0N  29853  lplncvrlvol2  29877  lplncvrlvol  29878  dalempnes  29913  dalemqnet  29914  dalemcea  29922  dalem3  29926  cdlema1N  30053  cdlemb  30056  paddasslem5  30086  llnexchb2lem  30130  osumcllem4N  30221  pexmidlem1N  30232  lhp2lt  30263  lhp2atne  30296  lhp2at0ne  30298  4atexlemunv  30328  4atexlemex2  30333  trlne  30447  trlval4  30450  cdlemc4  30456  cdleme11dN  30524  cdleme11h  30528  cdlemednuN  30562  cdleme20j  30580  cdleme20k  30581  cdleme21at  30590  cdleme35f  30716  cdlemg11b  30904  dia2dimlem1  31327  dihmeetlem3N  31568  dihmeetlem15N  31584  dochsnnz  31713  dochexmidlem1  31723  dochexmidlem7  31729  mapdindp3  31985
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 2450
  Copyright terms: Public domain W3C validator