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

Theorem necon3d 2675
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 2661 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2649 . 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 1370    =/= wne 2647
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 2649
This theorem is referenced by:  necon3iOLD  2692  pm13.18  2762  ssn0  3777  pssdifn0  3847  uniintsn  4272  suppssfvOLD  6425  suppssov1OLD  6426  ressuppssdif  6819  suppfnss  6823  suppssov1  6830  suppssfv  6834  omord  7116  nnmord  7180  mapdom2  7591  findcard2  7662  kmlem9  8437  isf32lem7  8638  1re  9495  addid1  9659  nn0n0n1ge2  10753  xnegdi  11321  fseqsupubi  11916  sqrgt0  12865  supcvg  13435  efne0  13498  pceulem  14029  pcqmul  14037  pcqcl  14040  pcaddlem  14067  pcadd  14068  grpinvnz  15715  symgfvne  16011  symg2bas  16021  odmulgeq  16178  gsumval3OLD  16502  gsumval3lem2  16504  gsumval3  16505  abvdom  17045  mptscmfsupp0  17133  lmodindp1  17217  lspsneleq  17318  lspsneq  17325  lspexch  17332  lspindp3  17339  lspsnsubn0  17343  rngelnzr  17469  coe1tmmul2  17852  ply1scln0  17867  dsmmsubg  18292  dsmmlss  18293  elfrlmbasn0  18314  mavmulsolcl  18488  0ntr  18806  elcls3  18818  neindisj  18852  neindisj2  18858  conndisj  19151  dfcon2  19154  fbunfip  19573  deg1mul2  21718  ply1nzb  21726  ne0p  21807  dgreq0  21864  dgradd2  21867  dgrcolem2  21873  elqaalem3  21919  logcj  22187  argimgt0  22193  tanarg  22200  ang180lem2  22338  ftalem2  22543  ftalem4  22545  ftalem5  22546  dvdssqf  22608  f1otrg  23268  f1otrge  23269  ax5seglem4  23329  ax5seglem5  23330  axeuclid  23360  axcontlem2  23362  axcontlem4  23364  nmlno0lem  24344  hlipgt0  24466  h1dn0  25106  spansneleq  25124  h1datomi  25135  nmlnop0iALT  25550  superpos  25909  chirredi  25949  ogrpaddlt  26325  qqhval2lem  26554  derangenlem  27202  subfacp1lem5  27215  ntrivcvgfvn0  27557  btwndiff  28201  btwnconn1lem7  28267  btwnconn1lem12  28272  tan2h  28571  dvcnsqr  28625  areacirclem1  28631  isdrngo2  28911  isdrngo3  28912  pell1234qrne0  29341  jm2.26lem3  29497  usgra2wlkspthlem1  30443  usgra2wlkspthlem2  30444  usgra2adedgspthlem2  30451  frgregordn0  30810  rng1ne0  30920  0rngnnzr  30925  domnmsuppn0  30929  rmsuppss  30930  scmsuppss  30932  lsatn0  32967  lsatspn0  32968  lkrlspeqN  33139  cvlsupr2  33311  dalem25  33665  4atexlemcnd  34039  ltrncnvnid  34094  trlator0  34138  ltrnnidn  34141  trlnid  34146  cdleme3b  34196  cdleme11l  34236  cdleme16b  34246  cdleme35h2  34424  cdleme38n  34431  cdlemg8c  34596  cdlemg11a  34604  cdlemg12e  34614  cdlemg18a  34645  trlcoat  34690  trlcone  34695  tendo1ne0  34795  cdleml9  34951  dvheveccl  35080  dihmeetlem13N  35287  dihlspsnat  35301  dihpN  35304  dihatexv  35306  dochsat  35351  dochkrshp  35354  dochkr1  35446  lcfrlem28  35538  lcfrlem32  35542  mapdn0  35637  mapdpglem11  35650  mapdpglem16  35655
  Copyright terms: Public domain W3C validator