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

Theorem con1d 124
Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992.)
Hypothesis
Ref Expression
con1d.1
Assertion
Ref Expression
con1d

Proof of Theorem con1d
StepHypRef Expression
1 con1d.1 . . 3
2 notnot1 122 . . 3
31, 2syl6 33 . 2
43con4d 105 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  mt3d  125  con1  128  con3d  133  pm2.24d  143  pm2.61d  158  pm2.8  850  dedlem0b  953  meredith  1472  hbnt  1894  axc11nlem  1938  axc11nlemOLD  2048  necon3bd  2669  necon1adOLD  2674  necon1bd  2675  necon4bdOLD  2680  sspss  3602  neldif  3628  ssonprc  6627  limsssuc  6685  limom  6715  onfununi  7031  pw2f1olem  7641  domtriord  7683  pssnn  7758  ordtypelem10  7973  rankxpsuc  8321  carden2a  8368  fidomtri2  8396  alephdom  8483  isf32lem12  8765  isfin1-3  8787  isfin7-2  8797  entric  8953  inttsk  9173  zeo  10973  zeo2  10974  uzwoOLD  11174  xrlttri  11374  xaddf  11452  elfzonelfzo  11912  fzonfzoufzol  11913  elfznelfzo  11915  om2uzf1oi  12064  hashnfinnn0  12432  ruclem3  13966  bitsinv1lem  14091  sadcaddlem  14107  phiprmpw  14306  iserodd  14359  fldivp1  14416  prmpwdvds  14422  vdwlem6  14504  sylow2alem2  16638  efgs1b  16754  fctop  19505  cctop  19507  ppttop  19508  iccpnfcnv  21444  iccpnfhmeo  21445  iscau2  21716  ovolicc2lem2  21929  mbfeqalem  22049  limccnp2  22296  radcnv0  22811  psercnlem1  22820  pserdvlem2  22823  logtayl  23041  cxpsqrt  23084  leibpilem1  23271  rlimcnp2  23296  amgm  23320  pntpbnd1  23771  pntlem3  23794  atssma  27297  spc2d  27373  supxrnemnf  27583  xrge0iifcnv  27915  eulerpartlemf  28309  arg-ax  29881  pw2f1ocnv  30979  pm10.57  31276  afvco2  32261  islininds2  33085  con5  33292  con3ALT  33300  bj-axc11nlemv  34315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator