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  826  dedlem0b  924  meredith  1400  ax12o10lem12  1646  ax12olem23  1657  19.9t  1761  necon3bd  2458  necon4bd  2483  necon1ad  2488  sspss  3250  neldif  3276  ssonprc  4555  limsssuc  4613  limom  4643  onfununi  6326  pw2f1olem  6934  domtriord  6975  pssnn  7049  ordtypelem10  7210  rankxpsuc  7520  carden2a  7567  fidomtri2  7595  alephdom  7676  isf32lem12  7958  isfin1-3  7980  isfin7-2  7990  entric  8147  inttsk  8364  zeo  10064  zeo2  10065  uzwoOLD  10249  xrlttri  10440  xaddf  10517  om2uzf1oi  10982  ruclem3  12473  bitsinv1lem  12594  sadcaddlem  12610  phiprmpw  12806  iserodd  12850  fldivp1  12907  prmpwdvds  12913  vdwlem6  12995  sylow2alem2  14891  efgs1b  15007  fctop  16703  cctop  16705  ppttop  16706  iccpnfcnv  18404  iccpnfhmeo  18405  iscau2  18665  ovolicc2lem2  18839  mbfeqalem  18959  limccnp2  19204  radcnv0  19754  psercnlem1  19763  pserdvlem2  19766  logtayl  19969  cxpsqr  20012  leibpilem1  20198  rlimcnp2  20223  amgm  20247  pntpbnd1  20697  pntlem3  20720  atssma  22918  arg-ax  24230  ltl4ev  24358  phthps  24362  pw2f1ocnv  26497  pm10.57  26933  con5  27338  con3ALT  27346  a4imfK  28165  ax12o10lem12K  28219  ax12o10lem12X  28220  ax12olem23X  28244  ax12-3  28271  a12study6  28285
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator