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

Theorem necon3d 2636
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 2634 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2600 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 219 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon3i  2637  pm13.18  2670  ssn0  3652  pssdifn0  3681  uniintsn  4079  suppssfv  6293  suppssov1  6294  omord  6803  nnmord  6867  mapdom2  7270  findcard2  7340  kmlem9  8030  isf32lem7  8231  1re  9082  addid1  9238  nn0n0n1ge2  10272  xnegdi  10819  fseqsupubi  11309  sqrgt0  12056  supcvg  12627  efne0  12690  pceulem  13211  pcqmul  13219  pcqcl  13222  pcaddlem  13249  pcadd  13250  grpinvnz  14854  odmulgeq  15185  gsumval3  15506  abvdom  15918  lmodindp1  16082  lspsneleq  16179  lspsneq  16186  lspexch  16193  lspindp3  16200  lspsnsubn0  16204  rngelnzr  16328  coe1tmmul2  16660  ply1scln0  16674  0ntr  17127  elcls3  17139  neindisj  17173  neindisj2  17179  conndisj  17471  dfcon2  17474  fbunfip  17893  deg1mul2  20029  ply1nzb  20037  ne0p  20118  dgreq0  20175  dgradd2  20178  dgrcolem2  20184  elqaalem3  20230  logcj  20493  argimgt0  20499  tanarg  20506  ang180lem2  20644  ftalem2  20848  ftalem4  20850  ftalem5  20851  dvdssqf  20913  nmlno0lem  22286  hlipgt0  22408  h1dn0  23046  spansneleq  23064  h1datomi  23075  nmlnop0iALT  23490  superpos  23849  chirredi  23889  ofldaddlt  24233  qqhval2lem  24357  derangenlem  24849  subfacp1lem5  24862  ntrivcvgfvn0  25219  ax5seglem4  25863  ax5seglem5  25864  axeuclid  25894  axcontlem2  25896  axcontlem4  25898  btwndiff  25953  btwnconn1lem7  26019  btwnconn1lem12  26024  dvreacos  26271  areacirclem2  26272  isdrngo2  26555  isdrngo3  26556  pell1234qrne0  26897  jm2.26lem3  27053  dsmmsubg  27167  dsmmlss  27168  usgra2wlkspthlem1  28249  usgra2wlkspthlem2  28250  usgra2adedgspthlem2  28257  frgregordn0  28386  lsatn0  29724  lsatspn0  29725  lkrlspeqN  29896  cvlsupr2  30068  dalem25  30422  4atexlemcnd  30796  ltrncnvnid  30851  trlator0  30895  ltrnnidn  30898  trlnid  30903  cdleme3b  30953  cdleme11l  30993  cdleme16b  31003  cdleme35h2  31181  cdleme38n  31188  cdlemg8c  31353  cdlemg11a  31361  cdlemg12e  31371  cdlemg18a  31402  trlcoat  31447  trlcone  31452  tendo1ne0  31552  cdleml9  31708  dvheveccl  31837  dihmeetlem13N  32044  dihlspsnat  32058  dihpN  32061  dihatexv  32063  dochsat  32108  dochkrshp  32111  dochkr1  32203  lcfrlem28  32295  lcfrlem32  32299  mapdn0  32394  mapdpglem11  32407  mapdpglem16  32412
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2600
  Copyright terms: Public domain W3C validator