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

Theorem necon3d 2665
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 2651 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2638 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 227 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1381    =/= wne 2636
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 2638
This theorem is referenced by:  necon3iOLD  2682  pm13.18  2752  ssn0  3800  pssdifn0  3870  uniintsn  4305  suppssfvOLD  6512  suppssov1OLD  6513  ressuppssdif  6919  suppfnss  6923  suppssov1  6930  suppssfv  6934  omord  7215  nnmord  7279  mapdom2  7686  findcard2  7758  kmlem9  8536  isf32lem7  8737  1re  9593  addid1  9758  nn0n0n1ge2  10860  xnegdi  11444  fseqsupubi  12062  sqrtgt0  13066  supcvg  13641  efne0  13704  pceulem  14241  pcqmul  14249  pcqcl  14252  pcaddlem  14279  pcadd  14280  grpinvnz  15978  symgfvne  16282  symg2bas  16292  odmulgeq  16448  gsumval3OLD  16777  gsumval3lem2  16779  gsumval3  16780  ring1ne0  17107  abvdom  17355  mptscmfsupp0  17444  lmodindp1  17528  lspsneleq  17629  lspsneq  17636  lspexch  17643  lspindp3  17650  lspsnsubn0  17654  ringelnzr  17782  0ringnnzr  17785  coe1tmmul2  18185  ply1scln0  18200  dsmmsubg  18641  dsmmlss  18642  elfrlmbasn0  18663  mavmulsolcl  18920  0ntr  19438  elcls3  19450  neindisj  19484  neindisj2  19490  conndisj  19783  dfcon2  19786  fbunfip  20236  deg1mul2  22381  ply1nzb  22389  ne0p  22470  dgreq0  22527  dgradd2  22530  dgrcolem2  22536  elqaalem3  22582  logcj  22856  argimgt0  22862  tanarg  22869  ang180lem2  23007  ftalem2  23212  ftalem4  23214  ftalem5  23215  dvdssqf  23277  lmimid  24024  lmiisolem  24026  hypcgrlem1  24029  hypcgrlem2  24030  f1otrg  24039  f1otrge  24040  ax5seglem4  24100  ax5seglem5  24101  axeuclid  24131  axcontlem2  24133  axcontlem4  24135  usgra2adedgspthlem2  24477  usgra2wlkspthlem1  24484  usgra2wlkspthlem2  24485  frgregordn0  24935  nmlno0lem  25573  hlipgt0  25695  h1dn0  26335  spansneleq  26353  h1datomi  26364  nmlnop0iALT  26779  superpos  27138  chirredi  27178  ogrpaddlt  27574  qqhval2lem  27828  derangenlem  28481  subfacp1lem5  28494  ntrivcvgfvn0  29001  btwndiff  29645  btwnconn1lem7  29711  btwnconn1lem12  29716  tan2h  30015  dvcnsqrt  30069  areacirclem1  30075  isdrngo2  30329  isdrngo3  30330  pell1234qrne0  30757  jm2.26lem3  30911  2zrngnmlid  32455  2zrngnmrid  32456  2zrngnmlid2  32457  domnmsuppn0  32672  rmsuppss  32673  scmsuppss  32675  lsatn0  34426  lsatspn0  34427  lkrlspeqN  34598  cvlsupr2  34770  dalem25  35124  4atexlemcnd  35498  ltrncnvnid  35553  trlator0  35598  ltrnnidn  35601  trlnid  35606  cdleme3b  35656  cdleme11l  35696  cdleme16b  35706  cdleme35h2  35885  cdleme38n  35892  cdlemg8c  36057  cdlemg11a  36065  cdlemg12e  36075  cdlemg18a  36106  trlcoat  36151  trlcone  36156  tendo1ne0  36256  cdleml9  36412  dvheveccl  36541  dihmeetlem13N  36748  dihlspsnat  36762  dihpN  36765  dihatexv  36767  dochsat  36812  dochkrshp  36815  dochkr1  36907  lcfrlem28  36999  lcfrlem32  37003  mapdn0  37098  mapdpglem11  37111  mapdpglem16  37116
  Copyright terms: Public domain W3C validator