Theorem necon3d 2815

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

Step	Hyp	Ref	Expression
1		necon3d.1	. . 3 |- ( ph -> ( A = B -> C = D ) )
2	1	necon3ad 2807	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2795	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	syl6ibr 242	1 |- ( ph -> ( C =/= D -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  pm13.18  2875  pssdifn0  3944  ssn0  3976  uniintsn  4514  funopsn  6413  f1prex  6539  ressuppssdif  7316  suppfnss  7320  suppssov1  7327  suppssfv  7331  omord  7648  nnmord  7712  mapdom2  8131  findcard2  8200  kmlem9  8980  isf32lem7  9181  1re  10039  addid1  10216  addn0nid  10451  nn0n0n1ge2  11358  xnegdi  12078  fseqsupubi  12777  sqrtgt0  13999  supcvg  14588  ntrivcvgfvn0  14631  efne0  14827  divgcdcoprmex  15380  pceulem  15550  pcqmul  15558  pcqcl  15561  pcaddlem  15592  pcadd  15593  grpinvnz  17486  symgfvne  17808  symg2bas  17818  odmulgeq  17974  gsumval3lem2  18307  gsumval3  18308  ring1ne0  18591  abvdom  18838  lmodfopne  18901  mptscmfsupp0  18928  lmodindp1  19014  lspsneleq  19115  lspsneq  19122  lspexch  19129  lspindp3  19136  lspsnsubn0  19140  ringelnzr  19266  0ringnnzr  19269  coe1tmmul2  19646  ply1scln0  19661  dsmmsubg  20087  dsmmlss  20088  elfrlmbasn0  20106  mavmulsolcl  20357  0ntr  20875  elcls3  20887  neindisj  20921  neindisj2  20927  conndisj  21219  dfconn2  21222  fbunfip  21673  deg1mul2  23874  ply1nzb  23882  ne0p  23963  dgreq0  24021  dgradd2  24024  dgrcolem2  24030  elqaalem3  24076  logcj  24352  argimgt0  24358  tanarg  24365  dvcnsqrt  24485  ang180lem2  24540  ftalem2  24800  ftalem4  24802  ftalem5  24803  dvdssqf  24864  mirhl2  25576  lmimid  25686  lmiisolem  25688  hypcgrlem1  25691  hypcgrlem2  25692  f1otrg  25751  f1otrge  25752  ax5seglem4  25812  ax5seglem5  25813  axeuclid  25843  axcontlem2  25845  axcontlem4  25847  pthdivtx  26625  spthdep  26630  usgr2wlkneq  26652  usgr2trlncl  26656  3pthdlem1  27024  uhgr3cyclexlem  27041  frgrwopreglem4a  27174  frrusgrord0lem  27203  nmlno0lem  27648  hlipgt0  27770  h1dn0  28411  spansneleq  28429  h1datomi  28440  nmlnop0iALT  28854  superpos  29213  chirredi  29253  ogrpaddlt  29718  psgnfzto1stlem  29850  qqhval2lem  30025  derangenlem  31153  subfacp1lem5  31166  scutbdaylt  31922  btwndiff  32134  btwnconn1lem7  32200  btwnconn1lem12  32205  tan2h  33401  poimirlem1  33410  poimirlem9  33418  poimirlem17  33426  poimirlem22  33431  areacirclem1  33500  isdrngo2  33757  isdrngo3  33758  lsatn0  34286  lsatspn0  34287  lkrlspeqN  34458  cvlsupr2  34630  dalem25  34984  4atexlemcnd  35358  ltrncnvnid  35413  trlator0  35458  ltrnnidn  35461  trlnid  35466  cdleme3b  35516  cdleme11l  35556  cdleme16b  35566  cdleme35h2  35745  cdleme38n  35752  cdlemg8c  35917  cdlemg11a  35925  cdlemg12e  35935  cdlemg18a  35966  trlcoat  36011  trlcone  36016  tendo1ne0  36116  cdleml9  36272  dvheveccl  36401  dihmeetlem13N  36608  dihlspsnat  36622  dihpN  36625  dihatexv  36627  dochsat  36672  dochkrshp  36675  dochkr1  36767  lcfrlem28  36859  lcfrlem32  36863  mapdn0  36958  mapdpglem11  36971  mapdpglem16  36976  pell1234qrne0  37417  jm2.26lem3  37568  2zrngnmlid  41949  2zrngnmrid  41950  2zrngnmlid2  41951  domnmsuppn0  42150  rmsuppss  42151  scmsuppss  42153  aacllem  42547