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

Theorem necon3d 2678
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 2664 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2651 . 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 1398    =/= wne 2649
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 2651
This theorem is referenced by:  necon3iOLD  2695  pm13.18  2765  ssn0  3817  pssdifn0  3876  uniintsn  4309  suppssfvOLD  6504  suppssov1OLD  6505  ressuppssdif  6913  suppfnss  6917  suppssov1  6924  suppssfv  6928  omord  7209  nnmord  7273  mapdom2  7681  findcard2  7752  kmlem9  8529  isf32lem7  8730  1re  9584  addid1  9749  nn0n0n1ge2  10855  xnegdi  11443  fseqsupubi  12070  sqrtgt0  13174  supcvg  13749  ntrivcvgfvn0  13790  efne0  13914  pceulem  14453  pcqmul  14461  pcqcl  14464  pcaddlem  14491  pcadd  14492  grpinvnz  16308  symgfvne  16612  symg2bas  16622  odmulgeq  16778  gsumval3OLD  17107  gsumval3lem2  17109  gsumval3  17110  ring1ne0  17434  abvdom  17682  mptscmfsupp0  17771  lmodindp1  17855  lspsneleq  17956  lspsneq  17963  lspexch  17970  lspindp3  17977  lspsnsubn0  17981  ringelnzr  18109  0ringnnzr  18112  coe1tmmul2  18512  ply1scln0  18527  dsmmsubg  18947  dsmmlss  18948  elfrlmbasn0  18967  mavmulsolcl  19220  0ntr  19739  elcls3  19751  neindisj  19785  neindisj2  19791  conndisj  20083  dfcon2  20086  fbunfip  20536  deg1mul2  22681  ply1nzb  22689  ne0p  22770  dgreq0  22828  dgradd2  22831  dgrcolem2  22837  elqaalem3  22883  logcj  23159  argimgt0  23165  tanarg  23172  ang180lem2  23341  ftalem2  23545  ftalem4  23547  ftalem5  23548  dvdssqf  23610  lmimid  24360  lmiisolem  24362  hypcgrlem1  24365  hypcgrlem2  24366  f1otrg  24376  f1otrge  24377  ax5seglem4  24437  ax5seglem5  24438  axeuclid  24468  axcontlem2  24470  axcontlem4  24472  usgra2adedgspthlem2  24814  usgra2wlkspthlem1  24821  usgra2wlkspthlem2  24822  frgregordn0  25272  nmlno0lem  25906  hlipgt0  26028  h1dn0  26668  spansneleq  26686  h1datomi  26697  nmlnop0iALT  27112  superpos  27471  chirredi  27511  ogrpaddlt  27942  qqhval2lem  28196  derangenlem  28879  subfacp1lem5  28892  btwndiff  29905  btwnconn1lem7  29971  btwnconn1lem12  29976  tan2h  30287  dvcnsqrt  30341  areacirclem1  30347  isdrngo2  30601  isdrngo3  30602  pell1234qrne0  31028  jm2.26lem3  31182  2zrngnmlid  33009  2zrngnmrid  33010  2zrngnmlid2  33011  domnmsuppn0  33216  rmsuppss  33217  scmsuppss  33219  aacllem  33604  lsatn0  35121  lsatspn0  35122  lkrlspeqN  35293  cvlsupr2  35465  dalem25  35819  4atexlemcnd  36193  ltrncnvnid  36248  trlator0  36293  ltrnnidn  36296  trlnid  36301  cdleme3b  36351  cdleme11l  36391  cdleme16b  36401  cdleme35h2  36580  cdleme38n  36587  cdlemg8c  36752  cdlemg11a  36760  cdlemg12e  36770  cdlemg18a  36801  trlcoat  36846  trlcone  36851  tendo1ne0  36951  cdleml9  37107  dvheveccl  37236  dihmeetlem13N  37443  dihlspsnat  37457  dihpN  37460  dihatexv  37462  dochsat  37507  dochkrshp  37510  dochkr1  37602  lcfrlem28  37694  lcfrlem32  37698  mapdn0  37793  mapdpglem11  37806  mapdpglem16  37811
  Copyright terms: Public domain W3C validator