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

Theorem necon3d 2484
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 2482 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2448 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 218 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon3i  2485  pm13.18  2518  ssn0  3487  pssdifn0  3515  uniintsn  3899  suppssfv  6074  suppssov1  6075  omord  6566  nnmord  6630  mapdom2  7032  findcard2  7098  kmlem9  7784  isf32lem7  7985  1re  8837  addid1  8992  xnegdi  10568  fseqsupubi  11040  sqrgt0  11744  supcvg  12314  efne0  12377  pceulem  12898  pcqmul  12906  pcqcl  12909  pcaddlem  12936  pcadd  12937  grpinvnz  14539  odmulgeq  14870  gsumval3  15191  abvdom  15603  lmodindp1  15771  lspsneleq  15868  lspsneq  15875  lspexch  15882  lspindp3  15889  lspsnsubn0  15893  rngelnzr  16017  coe1tmmul2  16352  ply1scln0  16366  0ntr  16808  elcls3  16820  neindisj  16854  neindisj2  16860  conndisj  17142  dfcon2  17145  fbunfip  17564  deg1mul2  19500  ply1nzb  19508  ne0p  19589  dgreq0  19646  dgradd2  19649  dgrcolem2  19655  elqaalem3  19701  logcj  19960  argimgt0  19966  tanarg  19970  ang180lem2  20108  ftalem2  20311  ftalem4  20313  ftalem5  20314  dvdssqf  20376  nmlno0lem  21371  hlipgt0  21493  h1dn0  22131  spansneleq  22149  h1datomi  22160  nmlnop0iALT  22575  superpos  22934  chirredi  22974  derangenlem  23702  subfacp1lem5  23715  ax5seglem4  24560  ax5seglem5  24561  axeuclid  24591  axcontlem2  24593  axcontlem4  24595  btwndiff  24650  btwnconn1lem7  24716  btwnconn1lem12  24721  dvreacos  24924  areacirclem2  24925  hdrmp  25706  isdrngo2  26589  isdrngo3  26590  pell1234qrne0  26938  jm2.26lem3  27094  dsmmsubg  27209  dsmmlss  27210  lsatn0  29189  lsatspn0  29190  lkrlspeqN  29361  cvlsupr2  29533  dalem25  29887  4atexlemcnd  30261  ltrncnvnid  30316  trlator0  30360  ltrnnidn  30363  trlnid  30368  cdleme3b  30418  cdleme11l  30458  cdleme16b  30468  cdleme35h2  30646  cdleme38n  30653  cdlemg8c  30818  cdlemg11a  30826  cdlemg12e  30836  cdlemg18a  30867  trlcoat  30912  trlcone  30917  tendo1ne0  31017  cdleml9  31173  dvheveccl  31302  dihmeetlem13N  31509  dihlspsnat  31523  dihpN  31526  dihatexv  31528  dochsat  31573  dochkrshp  31576  dochkr1  31668  lcfrlem28  31760  lcfrlem32  31764  mapdn0  31859  mapdpglem11  31872  mapdpglem16  31877
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 177  df-ne 2448
  Copyright terms: Public domain W3C validator