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

Theorem necon3d 2645
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 2637 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2624 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 231 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1444    =/= wne 2622
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 189  df-ne 2624
This theorem is referenced by:  pm13.18  2705  ssn0  3767  pssdifn0  3827  uniintsn  4272  f1prex  6182  ressuppssdif  6936  suppfnss  6940  suppssov1  6947  suppssfv  6951  omord  7269  nnmord  7333  mapdom2  7743  findcard2  7811  kmlem9  8588  isf32lem7  8789  1re  9642  addid1  9813  nn0n0n1ge2  10932  xnegdi  11534  fseqsupubi  12191  sqrtgt0  13322  supcvg  13914  ntrivcvgfvn0  13955  efne0  14151  pceulem  14795  pcqmul  14803  pcqcl  14806  pcaddlem  14833  pcadd  14834  grpinvnz  16725  symgfvne  17029  symg2bas  17039  odmulgeq  17208  gsumval3lem2  17540  gsumval3  17541  ring1ne0  17821  abvdom  18066  mptscmfsupp0  18153  lmodindp1  18237  lspsneleq  18338  lspsneq  18345  lspexch  18352  lspindp3  18359  lspsnsubn0  18363  ringelnzr  18490  0ringnnzr  18493  coe1tmmul2  18869  ply1scln0  18884  dsmmsubg  19306  dsmmlss  19307  elfrlmbasn0  19325  mavmulsolcl  19576  0ntr  20087  elcls3  20099  neindisj  20133  neindisj2  20139  conndisj  20431  dfcon2  20434  fbunfip  20884  deg1mul2  23063  ply1nzb  23071  ne0p  23161  dgreq0  23219  dgradd2  23222  dgrcolem2  23228  elqaalem3  23274  elqaalem3OLD  23277  logcj  23555  argimgt0  23561  tanarg  23568  dvcnsqrt  23684  ang180lem2  23739  ftalem2  23998  ftalem4  24000  ftalem5  24001  ftalem4OLD  24002  ftalem5OLD  24003  dvdssqf  24065  mirhl2  24726  lmimid  24836  lmiisolem  24838  hypcgrlem1  24841  hypcgrlem2  24842  f1otrg  24901  f1otrge  24902  ax5seglem4  24962  ax5seglem5  24963  axeuclid  24993  axcontlem2  24995  axcontlem4  24997  usgra2adedgspthlem2  25340  usgra2wlkspthlem1  25347  usgra2wlkspthlem2  25348  frgregordn0  25798  nmlno0lem  26434  hlipgt0  26566  h1dn0  27205  spansneleq  27223  h1datomi  27234  nmlnop0iALT  27648  superpos  28007  chirredi  28047  ogrpaddlt  28481  psgnfzto1stlem  28613  qqhval2lem  28785  derangenlem  29894  subfacp1lem5  29907  btwndiff  30794  btwnconn1lem7  30860  btwnconn1lem12  30865  tan2h  31937  poimirlem1  31941  poimirlem9  31949  poimirlem17  31957  poimirlem22  31962  areacirclem1  32032  isdrngo2  32197  isdrngo3  32198  lsatn0  32565  lsatspn0  32566  lkrlspeqN  32737  cvlsupr2  32909  dalem25  33263  4atexlemcnd  33637  ltrncnvnid  33692  trlator0  33737  ltrnnidn  33740  trlnid  33745  cdleme3b  33795  cdleme11l  33835  cdleme16b  33845  cdleme35h2  34024  cdleme38n  34031  cdlemg8c  34196  cdlemg11a  34204  cdlemg12e  34214  cdlemg18a  34245  trlcoat  34290  trlcone  34295  tendo1ne0  34395  cdleml9  34551  dvheveccl  34680  dihmeetlem13N  34887  dihlspsnat  34901  dihpN  34904  dihatexv  34906  dochsat  34951  dochkrshp  34954  dochkr1  35046  lcfrlem28  35138  lcfrlem32  35142  mapdn0  35237  mapdpglem11  35250  mapdpglem16  35255  pell1234qrne0  35699  jm2.26lem3  35856  funopsn  39018  2zrngnmlid  40002  2zrngnmrid  40003  2zrngnmlid2  40004  domnmsuppn0  40207  rmsuppss  40208  scmsuppss  40210  aacllem  40593
  Copyright terms: Public domain W3C validator