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

Theorem con2d 115
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1
Assertion
Ref Expression
con2d

Proof of Theorem con2d
StepHypRef Expression
1 notnot2 112 . . 3
2 con2d.1 . . 3
31, 2syl5 32 . 2
43con4d 105 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  con2  116  mt2d  117  pm3.2im  145  exists2  2389  necon3adOLD  2668  necon2bd  2672  necon4adOLD  2678  spcimegf  3188  spcegf  3190  spcimedv  3193  rspcimedv  3212  minel  3882  disjxun  4450  sotric  4831  sotrieq  4832  poirr2  5396  funun  5635  imadif  5668  soisoi  6224  onnminsb  6639  oneqmin  6640  ordunisuc2  6679  limsssuc  6685  tz7.48lem  7125  sdomdif  7685  pssinf  7750  unblem1  7792  supnub  7942  elirrv  8044  inf3lem6  8071  cantnflem1  8129  cantnflem1OLD  8152  cardne  8367  cardsdomel  8376  carddom2  8379  cardmin2  8400  alephnbtwn  8473  infdif2  8611  fin4en1  8710  fin23lem31  8744  isf32lem5  8758  isf34lem4  8778  cfpwsdom  8980  fpwwe2  9042  addnidpi  9300  genpnnp  9404  btwnnz  10964  prime  10968  qsqueeze  11429  xralrple  11433  xmullem2  11486  xmulneg1  11490  ssfzoulel  11906  elfznelfzob  11916  bcval4  12385  seqcoll  12512  hashtpg  12523  swrdnd  12657  swrd0  12658  fsumcvg  13534  fsumsplit  13562  fprodcvg  13737  fprodsplit  13770  dvdsle  14031  divalglem8  14058  bitsinv1lem  14091  pockthg  14424  prmunb  14432  vdwlem6  14504  ramlb  14537  gsumzsplit  16944  gsumzsplitOLD  16945  opsrtoslem2  18149  obselocv  18759  elcls  19574  fbasrn  20385  ufilb  20407  ufilmax  20408  rnelfmlem  20453  alexsubALTlem4  20550  tsmssplit  20654  recld2  21319  fsumharmonic  23341  chtub  23487  lgsne0  23608  axlowdim  24264  nbusgra  24428  nbgranself  24434  usgrasscusgra  24483  cyclnspth  24631  eupath2lem3  24979  cvnsym  27209  cvntr  27211  atcvati  27305  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemfrcn0  28468  ballotlemirc  28470  dfpo2  29184  wfrlem10  29352  sltres  29424  nodenselem5  29445  nocvxminlem  29450  nobndup  29460  nobnddown  29461  nofulllem5  29466  onsucconi  29902  onint1  29914  nn0prpw  30141  fdc  30238  rencldnfilem  30754  radcnvrat  31195  stoweidlem34  31816  lsatcvat  34775  hlrelat2  35127  ltltncvr  35147  islln2a  35241  islpln2a  35272  islvol2aN  35316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator