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

Theorem necon3d 2485
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 2483 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2449 . 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 2447
This theorem is referenced by:  necon3i  2486  pm13.18  2519  ssn0  3488  pssdifn0  3516  uniintsn  3900  suppssfv  6036  suppssov1  6037  omord  6562  nnmord  6626  mapdom2  7028  findcard2  7094  kmlem9  7780  isf32lem7  7981  1re  8833  addid1  8988  xnegdi  10564  fseqsupubi  11036  sqrgt0  11740  supcvg  12310  efne0  12373  pceulem  12894  pcqmul  12902  pcqcl  12905  pcaddlem  12932  pcadd  12933  grpinvnz  14535  odmulgeq  14866  gsumval3  15187  abvdom  15599  lmodindp1  15767  lspsneleq  15864  lspsneq  15871  lspexch  15878  lspindp3  15885  lspsnsubn0  15889  rngelnzr  16013  coe1tmmul2  16348  ply1scln0  16362  0ntr  16804  elcls3  16816  neindisj  16850  neindisj2  16856  conndisj  17138  dfcon2  17141  fbunfip  17560  deg1mul2  19496  ply1nzb  19504  ne0p  19585  dgreq0  19642  dgradd2  19645  dgrcolem2  19651  elqaalem3  19697  logcj  19956  argimgt0  19962  tanarg  19966  ang180lem2  20104  ftalem2  20307  ftalem4  20309  ftalem5  20310  dvdssqf  20372  nmlno0lem  21365  hlipgt0  21487  h1dn0  22127  spansneleq  22145  h1datomi  22156  nmlnop0iALT  22571  superpos  22930  chirredi  22970  derangenlem  23109  subfacp1lem5  23122  ax5seglem4  23970  ax5seglem5  23971  axeuclid  24001  axcontlem2  24003  axcontlem4  24005  btwndiff  24060  btwnconn1lem7  24126  btwnconn1lem12  24131  dvreacos  24334  areacirclem2  24335  hdrmp  25117  isdrngo2  26000  isdrngo3  26001  pell1234qrne0  26349  jm2.26lem3  26505  dsmmsubg  26620  dsmmlss  26621  lsatn0  28468  lsatspn0  28469  lkrlspeqN  28640  cvlsupr2  28812  dalem25  29166  4atexlemcnd  29540  ltrncnvnid  29595  trlator0  29639  ltrnnidn  29642  trlnid  29647  cdleme3b  29697  cdleme11l  29737  cdleme16b  29747  cdleme35h2  29925  cdleme38n  29932  cdlemg8c  30097  cdlemg11a  30105  cdlemg12e  30115  cdlemg18a  30146  trlcoat  30191  trlcone  30196  tendo1ne0  30296  cdleml9  30452  dvheveccl  30581  dihmeetlem13N  30788  dihlspsnat  30802  dihpN  30805  dihatexv  30807  dochsat  30852  dochkrshp  30855  dochkr1  30947  lcfrlem28  31039  lcfrlem32  31043  mapdn0  31138  mapdpglem11  31151  mapdpglem16  31156
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 2449
  Copyright terms: Public domain W3C validator