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

Theorem necon3d 2641
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 2639 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2603 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 220 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon3i  2645  pm13.18  2678  ssn0  3662  pssdifn0  3691  uniintsn  4089  suppssfv  6304  suppssov1  6305  omord  6814  nnmord  6878  mapdom2  7281  findcard2  7351  kmlem9  8043  isf32lem7  8244  1re  9095  addid1  9251  nn0n0n1ge2  10285  xnegdi  10832  fseqsupubi  11322  sqrgt0  12069  supcvg  12640  efne0  12703  pceulem  13224  pcqmul  13232  pcqcl  13235  pcaddlem  13262  pcadd  13263  grpinvnz  14867  odmulgeq  15198  gsumval3  15519  abvdom  15931  lmodindp1  16095  lspsneleq  16192  lspsneq  16199  lspexch  16206  lspindp3  16213  lspsnsubn0  16217  rngelnzr  16341  coe1tmmul2  16673  ply1scln0  16687  0ntr  17140  elcls3  17152  neindisj  17186  neindisj2  17192  conndisj  17484  dfcon2  17487  fbunfip  17906  deg1mul2  20042  ply1nzb  20050  ne0p  20131  dgreq0  20188  dgradd2  20191  dgrcolem2  20197  elqaalem3  20243  logcj  20506  argimgt0  20512  tanarg  20519  ang180lem2  20657  ftalem2  20861  ftalem4  20863  ftalem5  20864  dvdssqf  20926  nmlno0lem  22299  hlipgt0  22421  h1dn0  23059  spansneleq  23077  h1datomi  23088  nmlnop0iALT  23503  superpos  23862  chirredi  23902  ofldaddlt  24246  qqhval2lem  24370  derangenlem  24862  subfacp1lem5  24875  ntrivcvgfvn0  25232  ax5seglem4  25876  ax5seglem5  25877  axeuclid  25907  axcontlem2  25909  axcontlem4  25911  btwndiff  25966  btwnconn1lem7  26032  btwnconn1lem12  26037  tan2h  26252  dvreacos  26305  areacirclem1  26306  isdrngo2  26588  isdrngo3  26589  pell1234qrne0  26930  jm2.26lem3  27086  dsmmsubg  27200  dsmmlss  27201  usgra2wlkspthlem1  28344  usgra2wlkspthlem2  28345  usgra2adedgspthlem2  28352  frgregordn0  28533  lsatn0  29871  lsatspn0  29872  lkrlspeqN  30043  cvlsupr2  30215  dalem25  30569  4atexlemcnd  30943  ltrncnvnid  30998  trlator0  31042  ltrnnidn  31045  trlnid  31050  cdleme3b  31100  cdleme11l  31140  cdleme16b  31150  cdleme35h2  31328  cdleme38n  31335  cdlemg8c  31500  cdlemg11a  31508  cdlemg12e  31518  cdlemg18a  31549  trlcoat  31594  trlcone  31599  tendo1ne0  31699  cdleml9  31855  dvheveccl  31984  dihmeetlem13N  32191  dihlspsnat  32205  dihpN  32208  dihatexv  32210  dochsat  32255  dochkrshp  32258  dochkr1  32350  lcfrlem28  32442  lcfrlem32  32446  mapdn0  32541  mapdpglem11  32554  mapdpglem16  32559
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator