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 227 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369    =/= wne 2601
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 185  df-ne 2603
This theorem is referenced by:  necon3i  2645  pm13.18  2678  ssn0  3665  pssdifn0  3735  uniintsn  4160  suppssfvOLD  6311  suppssov1OLD  6312  ressuppssdif  6705  suppfnss  6709  suppssov1  6716  suppssfv  6720  omord  6999  nnmord  7063  mapdom2  7474  findcard2  7544  kmlem9  8319  isf32lem7  8520  1re  9377  addid1  9541  nn0n0n1ge2  10635  xnegdi  11203  fseqsupubi  11792  sqrgt0  12740  supcvg  13310  efne0  13373  pceulem  13904  pcqmul  13912  pcqcl  13915  pcaddlem  13942  pcadd  13943  grpinvnz  15588  symgfvne  15884  symg2bas  15894  odmulgeq  16049  gsumval3OLD  16373  gsumval3lem2  16375  gsumval3  16376  abvdom  16903  mptscmfsupp0  16991  lmodindp1  17075  lspsneleq  17176  lspsneq  17183  lspexch  17190  lspindp3  17197  lspsnsubn0  17201  rngelnzr  17327  coe1tmmul2  17709  ply1scln0  17723  dsmmsubg  18148  dsmmlss  18149  elfrlmbasn0  18170  mavmulsolcl  18342  0ntr  18655  elcls3  18667  neindisj  18701  neindisj2  18707  conndisj  19000  dfcon2  19003  fbunfip  19422  deg1mul2  21566  ply1nzb  21574  ne0p  21655  dgreq0  21712  dgradd2  21715  dgrcolem2  21721  elqaalem3  21767  logcj  22035  argimgt0  22041  tanarg  22048  ang180lem2  22186  ftalem2  22391  ftalem4  22393  ftalem5  22394  dvdssqf  22456  f1otrg  23085  f1otrge  23086  ax5seglem4  23146  ax5seglem5  23147  axeuclid  23177  axcontlem2  23179  axcontlem4  23181  nmlno0lem  24161  hlipgt0  24283  h1dn0  24923  spansneleq  24941  h1datomi  24952  nmlnop0iALT  25367  superpos  25726  chirredi  25766  ogrpaddlt  26149  qqhval2lem  26379  derangenlem  27028  subfacp1lem5  27041  ntrivcvgfvn0  27383  btwndiff  28027  btwnconn1lem7  28093  btwnconn1lem12  28098  tan2h  28395  dvcnsqr  28449  areacirclem1  28455  isdrngo2  28735  isdrngo3  28736  pell1234qrne0  29165  jm2.26lem3  29321  usgra2wlkspthlem1  30267  usgra2wlkspthlem2  30268  usgra2adedgspthlem2  30275  frgregordn0  30634  rng1ne0  30742  0rngnnzr  30747  domnmsuppn0  30751  rmsuppss  30752  scmsuppss  30754  pmatcollpw1lem4  30859  lsatn0  32537  lsatspn0  32538  lkrlspeqN  32709  cvlsupr2  32881  dalem25  33235  4atexlemcnd  33609  ltrncnvnid  33664  trlator0  33708  ltrnnidn  33711  trlnid  33716  cdleme3b  33766  cdleme11l  33806  cdleme16b  33816  cdleme35h2  33994  cdleme38n  34001  cdlemg8c  34166  cdlemg11a  34174  cdlemg12e  34184  cdlemg18a  34215  trlcoat  34260  trlcone  34265  tendo1ne0  34365  cdleml9  34521  dvheveccl  34650  dihmeetlem13N  34857  dihlspsnat  34871  dihpN  34874  dihatexv  34876  dochsat  34921  dochkrshp  34924  dochkr1  35016  lcfrlem28  35108  lcfrlem32  35112  mapdn0  35207  mapdpglem11  35220  mapdpglem16  35225
  Copyright terms: Public domain W3C validator