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

Theorem necon3d 2605
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 2603 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2569 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 219 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2567
This theorem is referenced by:  necon3i  2606  pm13.18  2639  ssn0  3620  pssdifn0  3649  uniintsn  4047  suppssfv  6260  suppssov1  6261  omord  6770  nnmord  6834  mapdom2  7237  findcard2  7307  kmlem9  7994  isf32lem7  8195  1re  9046  addid1  9202  nn0n0n1ge2  10236  xnegdi  10783  fseqsupubi  11272  sqrgt0  12019  supcvg  12590  efne0  12653  pceulem  13174  pcqmul  13182  pcqcl  13185  pcaddlem  13212  pcadd  13213  grpinvnz  14817  odmulgeq  15148  gsumval3  15469  abvdom  15881  lmodindp1  16045  lspsneleq  16142  lspsneq  16149  lspexch  16156  lspindp3  16163  lspsnsubn0  16167  rngelnzr  16291  coe1tmmul2  16623  ply1scln0  16637  0ntr  17090  elcls3  17102  neindisj  17136  neindisj2  17142  conndisj  17432  dfcon2  17435  fbunfip  17854  deg1mul2  19990  ply1nzb  19998  ne0p  20079  dgreq0  20136  dgradd2  20139  dgrcolem2  20145  elqaalem3  20191  logcj  20454  argimgt0  20460  tanarg  20467  ang180lem2  20605  ftalem2  20809  ftalem4  20811  ftalem5  20812  dvdssqf  20874  nmlno0lem  22247  hlipgt0  22369  h1dn0  23007  spansneleq  23025  h1datomi  23036  nmlnop0iALT  23451  superpos  23810  chirredi  23850  ofldaddlt  24194  qqhval2lem  24318  derangenlem  24810  subfacp1lem5  24823  ntrivcvgfvn0  25180  ax5seglem4  25775  ax5seglem5  25776  axeuclid  25806  axcontlem2  25808  axcontlem4  25810  btwndiff  25865  btwnconn1lem7  25931  btwnconn1lem12  25936  dvreacos  26180  areacirclem2  26181  isdrngo2  26464  isdrngo3  26465  pell1234qrne0  26806  jm2.26lem3  26962  dsmmsubg  27077  dsmmlss  27078  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2adedgspthlem2  28044  frgregordn0  28173  lsatn0  29482  lsatspn0  29483  lkrlspeqN  29654  cvlsupr2  29826  dalem25  30180  4atexlemcnd  30554  ltrncnvnid  30609  trlator0  30653  ltrnnidn  30656  trlnid  30661  cdleme3b  30711  cdleme11l  30751  cdleme16b  30761  cdleme35h2  30939  cdleme38n  30946  cdlemg8c  31111  cdlemg11a  31119  cdlemg12e  31129  cdlemg18a  31160  trlcoat  31205  trlcone  31210  tendo1ne0  31310  cdleml9  31466  dvheveccl  31595  dihmeetlem13N  31802  dihlspsnat  31816  dihpN  31819  dihatexv  31821  dochsat  31866  dochkrshp  31869  dochkr1  31961  lcfrlem28  32053  lcfrlem32  32057  mapdn0  32152  mapdpglem11  32165  mapdpglem16  32170
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 178  df-ne 2569
  Copyright terms: Public domain W3C validator