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

Theorem necon3d 2559
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 2557 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2523 . 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 1642    =/= wne 2521
This theorem is referenced by:  necon3i  2560  pm13.18  2593  ssn0  3563  pssdifn0  3591  uniintsn  3980  suppssfv  6161  suppssov1  6162  omord  6653  nnmord  6717  mapdom2  7120  findcard2  7188  kmlem9  7874  isf32lem7  8075  1re  8927  addid1  9082  xnegdi  10660  fseqsupubi  11132  sqrgt0  11840  supcvg  12411  efne0  12474  pceulem  12995  pcqmul  13003  pcqcl  13006  pcaddlem  13033  pcadd  13034  grpinvnz  14638  odmulgeq  14969  gsumval3  15290  abvdom  15702  lmodindp1  15870  lspsneleq  15967  lspsneq  15974  lspexch  15981  lspindp3  15988  lspsnsubn0  15992  rngelnzr  16116  coe1tmmul2  16451  ply1scln0  16465  0ntr  16914  elcls3  16926  neindisj  16960  neindisj2  16966  conndisj  17248  dfcon2  17251  fbunfip  17666  deg1mul2  19604  ply1nzb  19612  ne0p  19693  dgreq0  19750  dgradd2  19753  dgrcolem2  19759  elqaalem3  19805  logcj  20068  argimgt0  20074  tanarg  20081  ang180lem2  20219  ftalem2  20423  ftalem4  20425  ftalem5  20426  dvdssqf  20488  nmlno0lem  21485  hlipgt0  21607  h1dn0  22245  spansneleq  22263  h1datomi  22274  nmlnop0iALT  22689  superpos  23048  chirredi  23088  qqhval2lem  23638  derangenlem  24106  subfacp1lem5  24119  ntrivcvgfvn0  24528  ax5seglem4  25119  ax5seglem5  25120  axeuclid  25150  axcontlem2  25152  axcontlem4  25154  btwndiff  25209  btwnconn1lem7  25275  btwnconn1lem12  25280  dvreacos  25516  areacirclem2  25517  isdrngo2  25912  isdrngo3  25913  pell1234qrne0  26261  jm2.26lem3  26417  dsmmsubg  26532  dsmmlss  26533  nn0n0n1ge2  27452  lsatn0  29258  lsatspn0  29259  lkrlspeqN  29430  cvlsupr2  29602  dalem25  29956  4atexlemcnd  30330  ltrncnvnid  30385  trlator0  30429  ltrnnidn  30432  trlnid  30437  cdleme3b  30487  cdleme11l  30527  cdleme16b  30537  cdleme35h2  30715  cdleme38n  30722  cdlemg8c  30887  cdlemg11a  30895  cdlemg12e  30905  cdlemg18a  30936  trlcoat  30981  trlcone  30986  tendo1ne0  31086  cdleml9  31242  dvheveccl  31371  dihmeetlem13N  31578  dihlspsnat  31592  dihpN  31595  dihatexv  31597  dochsat  31642  dochkrshp  31645  dochkr1  31737  lcfrlem28  31829  lcfrlem32  31833  mapdn0  31928  mapdpglem11  31941  mapdpglem16  31946
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 2523
  Copyright terms: Public domain W3C validator