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

Theorem necon3d 2649
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 2635 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2621 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 231 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1438    =/= wne 2619
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 189  df-ne 2621
This theorem is referenced by:  necon3iOLD  2666  pm13.18  2736  ssn0  3796  pssdifn0  3856  uniintsn  4291  f1prex  6195  ressuppssdif  6945  suppfnss  6949  suppssov1  6956  suppssfv  6960  omord  7275  nnmord  7339  mapdom2  7747  findcard2  7815  kmlem9  8590  isf32lem7  8791  1re  9644  addid1  9815  nn0n0n1ge2  10934  xnegdi  11536  fseqsupubi  12192  sqrtgt0  13316  supcvg  13907  ntrivcvgfvn0  13948  efne0  14144  pceulem  14788  pcqmul  14796  pcqcl  14799  pcaddlem  14826  pcadd  14827  grpinvnz  16718  symgfvne  17022  symg2bas  17032  odmulgeq  17201  gsumval3lem2  17533  gsumval3  17534  ring1ne0  17814  abvdom  18059  mptscmfsupp0  18146  lmodindp1  18230  lspsneleq  18331  lspsneq  18338  lspexch  18345  lspindp3  18352  lspsnsubn0  18356  ringelnzr  18483  0ringnnzr  18486  coe1tmmul2  18862  ply1scln0  18877  dsmmsubg  19298  dsmmlss  19299  elfrlmbasn0  19317  mavmulsolcl  19568  0ntr  20079  elcls3  20091  neindisj  20125  neindisj2  20131  conndisj  20423  dfcon2  20426  fbunfip  20876  deg1mul2  23055  ply1nzb  23063  ne0p  23153  dgreq0  23211  dgradd2  23214  dgrcolem2  23220  elqaalem3  23266  elqaalem3OLD  23269  logcj  23547  argimgt0  23553  tanarg  23560  dvcnsqrt  23676  ang180lem2  23731  ftalem2  23990  ftalem4  23992  ftalem5  23993  ftalem4OLD  23994  ftalem5OLD  23995  dvdssqf  24057  mirhl2  24718  lmimid  24828  lmiisolem  24830  hypcgrlem1  24833  hypcgrlem2  24834  f1otrg  24893  f1otrge  24894  ax5seglem4  24954  ax5seglem5  24955  axeuclid  24985  axcontlem2  24987  axcontlem4  24989  usgra2adedgspthlem2  25332  usgra2wlkspthlem1  25339  usgra2wlkspthlem2  25340  frgregordn0  25790  nmlno0lem  26426  hlipgt0  26558  h1dn0  27197  spansneleq  27215  h1datomi  27226  nmlnop0iALT  27640  superpos  27999  chirredi  28039  ogrpaddlt  28482  psgnfzto1stlem  28615  qqhval2lem  28787  derangenlem  29896  subfacp1lem5  29909  btwndiff  30793  btwnconn1lem7  30859  btwnconn1lem12  30864  tan2h  31857  poimirlem1  31861  poimirlem9  31869  poimirlem17  31877  poimirlem22  31882  areacirclem1  31952  isdrngo2  32117  isdrngo3  32118  lsatn0  32490  lsatspn0  32491  lkrlspeqN  32662  cvlsupr2  32834  dalem25  33188  4atexlemcnd  33562  ltrncnvnid  33617  trlator0  33662  ltrnnidn  33665  trlnid  33670  cdleme3b  33720  cdleme11l  33760  cdleme16b  33770  cdleme35h2  33949  cdleme38n  33956  cdlemg8c  34121  cdlemg11a  34129  cdlemg12e  34139  cdlemg18a  34170  trlcoat  34215  trlcone  34220  tendo1ne0  34320  cdleml9  34476  dvheveccl  34605  dihmeetlem13N  34812  dihlspsnat  34826  dihpN  34829  dihatexv  34831  dochsat  34876  dochkrshp  34879  dochkr1  34971  lcfrlem28  35063  lcfrlem32  35067  mapdn0  35162  mapdpglem11  35175  mapdpglem16  35180  pell1234qrne0  35625  jm2.26lem3  35782  funopsn  38723  2zrngnmlid  39253  2zrngnmrid  39254  2zrngnmlid2  39255  domnmsuppn0  39460  rmsuppss  39461  scmsuppss  39463  aacllem  39846
  Copyright terms: Public domain W3C validator