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

Theorem con1d 116
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 114 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 29 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
-.  ch ) )
43con4d 97 1  |-  ( ph  ->  ( -.  ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3d  117  con1  120  con3d  125  pm2.24d  135  pm2.61d  150  pm2.8  823  dedlem0b  919  meredith  1394  19.9ht  1726  19.9t  1782  ax12olem3  1870  necon3bd  2483  necon4bd  2508  necon1ad  2513  sspss  3275  neldif  3301  ssonprc  4583  limsssuc  4641  limom  4671  onfununi  6358  pw2f1olem  6966  domtriord  7007  pssnn  7081  ordtypelem10  7242  rankxpsuc  7552  carden2a  7599  fidomtri2  7627  alephdom  7708  isf32lem12  7990  isfin1-3  8012  isfin7-2  8022  entric  8179  inttsk  8396  zeo  10097  zeo2  10098  uzwoOLD  10282  xrlttri  10473  xaddf  10551  om2uzf1oi  11016  ruclem3  12511  bitsinv1lem  12632  sadcaddlem  12648  phiprmpw  12844  iserodd  12888  fldivp1  12945  prmpwdvds  12951  vdwlem6  13033  sylow2alem2  14929  efgs1b  15045  fctop  16741  cctop  16743  ppttop  16744  iccpnfcnv  18442  iccpnfhmeo  18443  iscau2  18703  ovolicc2lem2  18877  mbfeqalem  18997  limccnp2  19242  radcnv0  19792  psercnlem1  19801  pserdvlem2  19804  logtayl  20007  cxpsqr  20050  leibpilem1  20236  rlimcnp2  20261  amgm  20285  pntpbnd1  20735  pntlem3  20758  atssma  22958  supxrnemnf  23256  xrge0iifcnv  23315  arg-ax  24855  ltl4ev  24992  phthps  24996  pw2f1ocnv  27130  pm10.57  27566  afvco2  28037  con5  28285  con3ALT  28293  ax12-3  29104  a12study6  29118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator