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

Theorem necon3d 2486
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 2484 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2450 . 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 1625    =/= wne 2448
This theorem is referenced by:  necon3i  2487  pm13.18  2520  ssn0  3489  pssdifn0  3517  uniintsn  3901  suppssfv  6076  suppssov1  6077  omord  6568  nnmord  6632  mapdom2  7034  findcard2  7100  kmlem9  7786  isf32lem7  7987  1re  8839  addid1  8994  xnegdi  10570  fseqsupubi  11042  sqrgt0  11746  supcvg  12316  efne0  12379  pceulem  12900  pcqmul  12908  pcqcl  12911  pcaddlem  12938  pcadd  12939  grpinvnz  14541  odmulgeq  14872  gsumval3  15193  abvdom  15605  lmodindp1  15773  lspsneleq  15870  lspsneq  15877  lspexch  15884  lspindp3  15891  lspsnsubn0  15895  rngelnzr  16019  coe1tmmul2  16354  ply1scln0  16368  0ntr  16810  elcls3  16822  neindisj  16856  neindisj2  16862  conndisj  17144  dfcon2  17147  fbunfip  17566  deg1mul2  19502  ply1nzb  19510  ne0p  19591  dgreq0  19648  dgradd2  19651  dgrcolem2  19657  elqaalem3  19703  logcj  19962  argimgt0  19968  tanarg  19972  ang180lem2  20110  ftalem2  20313  ftalem4  20315  ftalem5  20316  dvdssqf  20378  nmlno0lem  21373  hlipgt0  21495  h1dn0  22133  spansneleq  22151  h1datomi  22162  nmlnop0iALT  22577  superpos  22936  chirredi  22976  derangenlem  23704  subfacp1lem5  23717  ax5seglem4  24562  ax5seglem5  24563  axeuclid  24593  axcontlem2  24595  axcontlem4  24597  btwndiff  24652  btwnconn1lem7  24718  btwnconn1lem12  24723  dvreacos  24926  areacirclem2  24936  hdrmp  25717  isdrngo2  26600  isdrngo3  26601  pell1234qrne0  26949  jm2.26lem3  27105  dsmmsubg  27220  dsmmlss  27221  lsatn0  29262  lsatspn0  29263  lkrlspeqN  29434  cvlsupr2  29606  dalem25  29960  4atexlemcnd  30334  ltrncnvnid  30389  trlator0  30433  ltrnnidn  30436  trlnid  30441  cdleme3b  30491  cdleme11l  30531  cdleme16b  30541  cdleme35h2  30719  cdleme38n  30726  cdlemg8c  30891  cdlemg11a  30899  cdlemg12e  30909  cdlemg18a  30940  trlcoat  30985  trlcone  30990  tendo1ne0  31090  cdleml9  31246  dvheveccl  31375  dihmeetlem13N  31582  dihlspsnat  31596  dihpN  31599  dihatexv  31601  dochsat  31646  dochkrshp  31649  dochkr1  31741  lcfrlem28  31833  lcfrlem32  31837  mapdn0  31932  mapdpglem11  31945  mapdpglem16  31950
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 2450
  Copyright terms: Public domain W3C validator