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

Theorem necon3d 2588
Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
Hypothesis
Ref Expression
necon3d.1  |-  ( ph  ->  ( A  =  B  ->  C  =  D ) )
Assertion
Ref Expression
necon3d  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )

Proof of Theorem necon3d
StepHypRef Expression
1 necon3d.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  C  =  D ) )
21necon3ad 2586 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2552 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 219 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2550
This theorem is referenced by:  necon3i  2589  pm13.18  2622  ssn0  3603  pssdifn0  3632  uniintsn  4029  suppssfv  6240  suppssov1  6241  omord  6747  nnmord  6811  mapdom2  7214  findcard2  7284  kmlem9  7971  isf32lem7  8172  1re  9023  addid1  9178  nn0n0n1ge2  10212  xnegdi  10759  fseqsupubi  11244  sqrgt0  11991  supcvg  12562  efne0  12625  pceulem  13146  pcqmul  13154  pcqcl  13157  pcaddlem  13184  pcadd  13185  grpinvnz  14789  odmulgeq  15120  gsumval3  15441  abvdom  15853  lmodindp1  16017  lspsneleq  16114  lspsneq  16121  lspexch  16128  lspindp3  16135  lspsnsubn0  16139  rngelnzr  16263  coe1tmmul2  16595  ply1scln0  16609  0ntr  17058  elcls3  17070  neindisj  17104  neindisj2  17110  conndisj  17400  dfcon2  17403  fbunfip  17822  deg1mul2  19904  ply1nzb  19912  ne0p  19993  dgreq0  20050  dgradd2  20053  dgrcolem2  20059  elqaalem3  20105  logcj  20368  argimgt0  20374  tanarg  20381  ang180lem2  20519  ftalem2  20723  ftalem4  20725  ftalem5  20726  dvdssqf  20788  nmlno0lem  22142  hlipgt0  22264  h1dn0  22902  spansneleq  22920  h1datomi  22931  nmlnop0iALT  23346  superpos  23705  chirredi  23745  ofldaddlt  24067  qqhval2lem  24164  derangenlem  24636  subfacp1lem5  24649  ntrivcvgfvn0  25006  ax5seglem4  25585  ax5seglem5  25586  axeuclid  25616  axcontlem2  25618  axcontlem4  25620  btwndiff  25675  btwnconn1lem7  25741  btwnconn1lem12  25746  dvreacos  25981  areacirclem2  25982  isdrngo2  26265  isdrngo3  26266  pell1234qrne0  26607  jm2.26lem3  26763  dsmmsubg  26878  dsmmlss  26879  lsatn0  29114  lsatspn0  29115  lkrlspeqN  29286  cvlsupr2  29458  dalem25  29812  4atexlemcnd  30186  ltrncnvnid  30241  trlator0  30285  ltrnnidn  30288  trlnid  30293  cdleme3b  30343  cdleme11l  30383  cdleme16b  30393  cdleme35h2  30571  cdleme38n  30578  cdlemg8c  30743  cdlemg11a  30751  cdlemg12e  30761  cdlemg18a  30792  trlcoat  30837  trlcone  30842  tendo1ne0  30942  cdleml9  31098  dvheveccl  31227  dihmeetlem13N  31434  dihlspsnat  31448  dihpN  31451  dihatexv  31453  dochsat  31498  dochkrshp  31501  dochkr1  31593  lcfrlem28  31685  lcfrlem32  31689  mapdn0  31784  mapdpglem11  31797  mapdpglem16  31802
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 178  df-ne 2552
  Copyright terms: Public domain W3C validator