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

Theorem con1d 124
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
con1d.1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Assertion
Ref Expression
con1d  |-  ( ph  ->  ( -.  ch  ->  ps ) )

Proof of Theorem con1d
StepHypRef Expression
1 con1d.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  ch ) )
2 notnot1 122 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 33 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
-.  ch ) )
43con4d 105 1  |-  ( ph  ->  ( -.  ch  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt3d  125  con1  128  con3d  133  pm2.24d  143  pm2.61d  158  pm2.8  841  dedlem0b  939  meredith  1451  hbnt  1832  axc11nlem  2001  necon3bd  2643  necon4bd  2671  necon1ad  2676  sspss  3452  neldif  3478  ssonprc  6402  limsssuc  6460  limom  6490  onfununi  6798  pw2f1olem  7411  domtriord  7453  pssnn  7527  ordtypelem10  7737  rankxpsuc  8085  carden2a  8132  fidomtri2  8160  alephdom  8247  isf32lem12  8529  isfin1-3  8551  isfin7-2  8561  entric  8717  inttsk  8937  zeo  10723  zeo2  10724  uzwoOLD  10914  xrlttri  11112  xaddf  11190  elfzonelfzo  11623  fzonfzoufzol  11624  elfznelfzo  11626  om2uzf1oi  11772  hashnfinnn0  12126  ruclem3  13511  bitsinv1lem  13633  sadcaddlem  13649  phiprmpw  13847  iserodd  13898  fldivp1  13955  prmpwdvds  13961  vdwlem6  14043  sylow2alem2  16110  efgs1b  16226  fctop  18508  cctop  18510  ppttop  18511  iccpnfcnv  20416  iccpnfhmeo  20417  iscau2  20688  ovolicc2lem2  20901  mbfeqalem  21020  limccnp2  21267  radcnv0  21824  psercnlem1  21833  pserdvlem2  21836  logtayl  22048  cxpsqr  22091  leibpilem1  22278  rlimcnp2  22303  amgm  22327  pntpbnd1  22778  pntlem3  22801  atssma  25701  spc2d  25777  supxrnemnf  25973  xrge0iifcnv  26283  eulerpartlemf  26667  arg-ax  28176  pw2f1ocnv  29295  pm10.57  29532  afvco2  29991  islininds2  30842  con5  31043  con3ALT  31051  bj-axc11nlemv  31996
  Copyright terms: Public domain W3C validator