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

Theorem necon3d 2691
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 2677 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2664 . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon3iOLD  2708  pm13.18  2778  ssn0  3818  pssdifn0  3888  uniintsn  4319  suppssfvOLD  6513  suppssov1OLD  6514  ressuppssdif  6918  suppfnss  6922  suppssov1  6929  suppssfv  6933  omord  7214  nnmord  7278  mapdom2  7685  findcard2  7756  kmlem9  8534  isf32lem7  8735  1re  9591  addid1  9755  nn0n0n1ge2  10855  xnegdi  11436  fseqsupubi  12052  sqrtgt0  13051  supcvg  13626  efne0  13689  pceulem  14224  pcqmul  14232  pcqcl  14235  pcaddlem  14262  pcadd  14263  grpinvnz  15910  symgfvne  16208  symg2bas  16218  odmulgeq  16375  gsumval3OLD  16699  gsumval3lem2  16701  gsumval3  16702  abvdom  17270  mptscmfsupp0  17359  lmodindp1  17443  lspsneleq  17544  lspsneq  17551  lspexch  17558  lspindp3  17565  lspsnsubn0  17569  rngelnzr  17695  coe1tmmul2  18088  ply1scln0  18103  dsmmsubg  18541  dsmmlss  18542  elfrlmbasn0  18563  mavmulsolcl  18820  0ntr  19338  elcls3  19350  neindisj  19384  neindisj2  19390  conndisj  19683  dfcon2  19686  fbunfip  20105  deg1mul2  22250  ply1nzb  22258  ne0p  22339  dgreq0  22396  dgradd2  22399  dgrcolem2  22405  elqaalem3  22451  logcj  22719  argimgt0  22725  tanarg  22732  ang180lem2  22870  ftalem2  23075  ftalem4  23077  ftalem5  23078  dvdssqf  23140  lmimid  23836  lmiisolem  23838  hypcgrlem1  23841  hypcgrlem2  23842  f1otrg  23850  f1otrge  23851  ax5seglem4  23911  ax5seglem5  23912  axeuclid  23942  axcontlem2  23944  axcontlem4  23946  usgra2adedgspthlem2  24288  usgra2wlkspthlem1  24295  usgra2wlkspthlem2  24296  frgregordn0  24747  nmlno0lem  25384  hlipgt0  25506  h1dn0  26146  spansneleq  26164  h1datomi  26175  nmlnop0iALT  26590  superpos  26949  chirredi  26989  ogrpaddlt  27370  qqhval2lem  27598  derangenlem  28255  subfacp1lem5  28268  ntrivcvgfvn0  28610  btwndiff  29254  btwnconn1lem7  29320  btwnconn1lem12  29325  tan2h  29624  dvcnsqrt  29678  areacirclem1  29684  isdrngo2  29964  isdrngo3  29965  pell1234qrne0  30393  jm2.26lem3  30547  rng1ne0  32026  0rngnnzr  32031  domnmsuppn0  32035  rmsuppss  32036  scmsuppss  32038  lsatn0  33796  lsatspn0  33797  lkrlspeqN  33968  cvlsupr2  34140  dalem25  34494  4atexlemcnd  34868  ltrncnvnid  34923  trlator0  34967  ltrnnidn  34970  trlnid  34975  cdleme3b  35025  cdleme11l  35065  cdleme16b  35075  cdleme35h2  35253  cdleme38n  35260  cdlemg8c  35425  cdlemg11a  35433  cdlemg12e  35443  cdlemg18a  35474  trlcoat  35519  trlcone  35524  tendo1ne0  35624  cdleml9  35780  dvheveccl  35909  dihmeetlem13N  36116  dihlspsnat  36130  dihpN  36133  dihatexv  36135  dochsat  36180  dochkrshp  36183  dochkr1  36275  lcfrlem28  36367  lcfrlem32  36371  mapdn0  36466  mapdpglem11  36479  mapdpglem16  36484
  Copyright terms: Public domain W3C validator