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

Theorem con1d 118
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 116 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 31 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
-.  ch ) )
43con4d 99 1  |-  ( ph  ->  ( -.  ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt3d  119  con1  122  con3d  127  pm2.24d  137  pm2.61d  152  pm2.8  825  dedlem0b  921  meredith  1396  19.9ht  1727  19.9t  1783  ax12olem3  1871  necon3bd  2484  necon4bd  2509  necon1ad  2514  sspss  3276  neldif  3302  ssonprc  4582  limsssuc  4640  limom  4670  onfununi  6353  pw2f1olem  6961  domtriord  7002  pssnn  7076  ordtypelem10  7237  rankxpsuc  7547  carden2a  7594  fidomtri2  7622  alephdom  7703  isf32lem12  7985  isfin1-3  8007  isfin7-2  8017  entric  8174  inttsk  8391  zeo  10092  zeo2  10093  uzwoOLD  10277  xrlttri  10468  xaddf  10545  om2uzf1oi  11010  ruclem3  12505  bitsinv1lem  12626  sadcaddlem  12642  phiprmpw  12838  iserodd  12882  fldivp1  12939  prmpwdvds  12945  vdwlem6  13027  sylow2alem2  14923  efgs1b  15039  fctop  16735  cctop  16737  ppttop  16738  iccpnfcnv  18436  iccpnfhmeo  18437  iscau2  18697  ovolicc2lem2  18871  mbfeqalem  18991  limccnp2  19236  radcnv0  19786  psercnlem1  19795  pserdvlem2  19798  logtayl  20001  cxpsqr  20044  leibpilem1  20230  rlimcnp2  20255  amgm  20279  pntpbnd1  20729  pntlem3  20752  atssma  22950  arg-ax  24262  ltl4ev  24390  phthps  24394  pw2f1ocnv  26529  pm10.57  26965  afvco2  27414  con5  27556  con3ALT  27564  ax12-3  28371  a12study6  28385
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator