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

Theorem necon3bd 2655
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 2644 . . 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 1383    =/= wne 2638
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 2640
This theorem is referenced by:  necon2ad  2656  nelne1  2772  nelne2  2773  nssne1  3545  nssne2  3546  disjne  3858  difsn  4149  nbrne1  4454  nbrne2  4455  peano5  6708  oeeui  7253  domdifsn  7602  ac6sfi  7766  inf3lem2  8049  cnfcom3lem  8150  cnfcom3lemOLD  8158  dfac9  8519  fin23lem21  8722  dedekindle  9748  zneo  10952  modirr  12038  sqrmo  13066  pc2dvds  14383  pcadd  14389  4sqlem11  14454  latnlej  15676  sylow2blem3  16620  irredn0  17330  irredn1  17333  lssneln0  17576  lspsnne2  17742  lspfixed  17752  lspindpi  17756  lsmcv  17765  lspsolv  17767  isnzr2  17889  coe1tmmul  18296  dfac14  20096  fbdmn0  20312  filufint  20398  flimfnfcls  20506  alexsubALTlem2  20525  evth  21436  cphsqrtcl2  21610  ovolicc2lem4  21908  lhop1lem  22391  lhop1  22392  lhop2  22393  lhop  22394  deg1add  22481  abelthlem2  22803  logcnlem2  23000  angpined  23137  asinneg  23193  lgsne0  23584  lgsqr  23597  lgsquadlem2  23606  lgsquadlem3  23607  axlowdimlem17  24237  dvrunz  25411  spansncvi  26546  dmgmaddn0  28542  broutsideof2  29747  dvasin  30078  dvacos  30079  nninfnub  30219  pellexlem1  30740  dfac21  30987  pm13.14  31270  uzlidlring  32445  lsatcvatlem  34514  lkrlsp2  34568  opnlen0  34653  2llnne2N  34872  lnnat  34891  llnn0  34980  lplnn0N  35011  lplnllnneN  35020  llncvrlpln2  35021  llncvrlpln  35022  lvoln0N  35055  lplncvrlvol2  35079  lplncvrlvol  35080  dalempnes  35115  dalemqnet  35116  dalemcea  35124  dalem3  35128  cdlema1N  35255  cdlemb  35258  paddasslem5  35288  llnexchb2lem  35332  osumcllem4N  35423  pexmidlem1N  35434  lhp2lt  35465  lhp2atne  35498  lhp2at0ne  35500  4atexlemunv  35530  4atexlemex2  35535  trlne  35650  trlval4  35653  cdlemc4  35659  cdleme11dN  35727  cdleme11h  35731  cdlemednuN  35765  cdleme20j  35784  cdleme20k  35785  cdleme21at  35794  cdleme35f  35920  cdlemg11b  36108  dia2dimlem1  36531  dihmeetlem3N  36772  dihmeetlem15N  36788  dochsnnz  36917  dochexmidlem1  36927  dochexmidlem7  36933  mapdindp3  37189
  Copyright terms: Public domain W3C validator