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

Theorem necon3bd 2679
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 2668 . . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon2ad  2680  nelne1  2796  nelne2  2797  nssne1  3565  nssne2  3566  disjne  3877  difsn  4167  nbrne1  4470  nbrne2  4471  peano5  6718  oeeui  7263  domdifsn  7612  ac6sfi  7776  inf3lem2  8058  cnfcom3lem  8159  cnfcom3lemOLD  8167  dfac9  8528  fin23lem21  8731  dedekindle  9756  zneo  10955  modirr  12037  sqrmo  13065  pc2dvds  14278  pcadd  14284  4sqlem11  14349  latnlej  15572  sylow2blem3  16515  irredn0  17224  irredn1  17227  lssneln0  17469  lspsnne2  17635  lspfixed  17645  lspindpi  17649  lsmcv  17658  lspsolv  17660  isnzr2  17781  coe1tmmul  18188  dfac14  19987  fbdmn0  20203  filufint  20289  flimfnfcls  20397  alexsubALTlem2  20416  evth  21327  cphsqrtcl2  21501  ovolicc2lem4  21799  lhop1lem  22282  lhop1  22283  lhop2  22284  lhop  22285  deg1add  22372  abelthlem2  22694  logcnlem2  22890  angpined  23027  asinneg  23083  lgsne0  23474  lgsqr  23487  lgsquadlem2  23496  lgsquadlem3  23497  axlowdimlem17  24084  dvrunz  25258  spansncvi  26393  dmgmaddn0  28390  broutsideof2  29699  dvasin  30030  dvacos  30031  nninfnub  30171  pellexlem1  30693  dfac21  30940  pm13.14  31218  uzlidlring  32329  lsatcvatlem  34247  lkrlsp2  34301  opnlen0  34386  2llnne2N  34605  lnnat  34624  llnn0  34713  lplnn0N  34744  lplnllnneN  34753  llncvrlpln2  34754  llncvrlpln  34755  lvoln0N  34788  lplncvrlvol2  34812  lplncvrlvol  34813  dalempnes  34848  dalemqnet  34849  dalemcea  34857  dalem3  34861  cdlema1N  34988  cdlemb  34991  paddasslem5  35021  llnexchb2lem  35065  osumcllem4N  35156  pexmidlem1N  35167  lhp2lt  35198  lhp2atne  35231  lhp2at0ne  35233  4atexlemunv  35263  4atexlemex2  35268  trlne  35382  trlval4  35385  cdlemc4  35391  cdleme11dN  35459  cdleme11h  35463  cdlemednuN  35497  cdleme20j  35515  cdleme20k  35516  cdleme21at  35525  cdleme35f  35651  cdlemg11b  35839  dia2dimlem1  36262  dihmeetlem3N  36503  dihmeetlem15N  36519  dochsnnz  36648  dochexmidlem1  36658  dochexmidlem7  36664  mapdindp3  36920
  Copyright terms: Public domain W3C validator