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

Theorem necon3bd 2558
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 2525 . . 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 1642    =/= wne 2521
This theorem is referenced by:  nelne1  2610  nelne2  2611  nssne1  3310  nssne2  3311  disjne  3576  difsn  3831  nbrne1  4121  nbrne2  4122  peano5  4761  oeeui  6687  domdifsn  7033  ac6sfi  7191  inf3lem2  7420  cnfcom3lem  7496  dfac9  7852  fin23lem21  8055  zneo  10186  modirr  11101  sqrmo  11833  pc2dvds  13028  pcadd  13034  4sqlem11  13099  latnlej  14273  sylow2blem3  15032  irredn0  15584  irredn1  15587  lssneln0  15808  lspsnne2  15970  lspfixed  15980  lspindpi  15984  lsmcv  15993  lspsolv  15995  isnzr2  16114  coe1tmmul  16452  dfac14  17418  fbdmn0  17631  filufint  17717  flimfnfcls  17825  alexsubALTlem2  17844  evth  18561  cphsqrcl2  18726  ovolicc2lem4  18983  lhop1lem  19464  lhop1  19465  lhop2  19466  lhop  19467  deg1add  19593  abelthlem2  19915  logcnlem2  20101  angpined  20238  asinneg  20293  lgsne0  20684  lgsqr  20697  lgsquadlem2  20706  lgsquadlem3  20707  dvrunz  21212  spansncvi  22345  dmgmaddn0  24056  dedekindle  24489  axlowdimlem17  25145  broutsideof2  25304  dvreasin  25515  nninfnub  25785  pellexlem1  26237  dfac21  26487  pm13.14  26932  lsatcvatlem  29308  lkrlsp2  29362  opnlen0  29447  2llnne2N  29666  lnnat  29685  llnn0  29774  lplnn0N  29805  lplnllnneN  29814  llncvrlpln2  29815  llncvrlpln  29816  lvoln0N  29849  lplncvrlvol2  29873  lplncvrlvol  29874  dalempnes  29909  dalemqnet  29910  dalemcea  29918  dalem3  29922  cdlema1N  30049  cdlemb  30052  paddasslem5  30082  llnexchb2lem  30126  osumcllem4N  30217  pexmidlem1N  30228  lhp2lt  30259  lhp2atne  30292  lhp2at0ne  30294  4atexlemunv  30324  4atexlemex2  30329  trlne  30443  trlval4  30446  cdlemc4  30452  cdleme11dN  30520  cdleme11h  30524  cdlemednuN  30558  cdleme20j  30576  cdleme20k  30577  cdleme21at  30586  cdleme35f  30712  cdlemg11b  30900  dia2dimlem1  31323  dihmeetlem3N  31564  dihmeetlem15N  31580  dochsnnz  31709  dochexmidlem1  31719  dochexmidlem7  31725  mapdindp3  31981
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 2523
  Copyright terms: Public domain W3C validator