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

Step	Hyp	Ref	Expression
1		con1d.1	. . 3 |- ( ph -> ( -. ps -> ch ) )
2		notnot1 116	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 31	. 2 |- ( ph -> ( -. ps -> -. -. ch ) )
4	3	con4d 99	1 |- ( ph -> ( -. ch -> ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  mt3d  119  con1  122  con3d  127  pm2.24d  137  pm2.61d  152  pm2.8  824  dedlem0b  920  meredith  1410  hbnt  1795  19.9htOLD  1799  19.9tOLD  1876  ax12olem3OLD  1979  ax10lem2  1989  necon3bd  2604  necon4bd  2629  necon1ad  2634  sspss  3406  neldif  3432  ssonprc  4731  limsssuc  4789  limom  4819  onfununi  6562  pw2f1olem  7171  domtriord  7212  pssnn  7286  ordtypelem10  7452  rankxpsuc  7762  carden2a  7809  fidomtri2  7837  alephdom  7918  isf32lem12  8200  isfin1-3  8222  isfin7-2  8232  entric  8388  inttsk  8605  zeo  10311  zeo2  10312  uzwoOLD  10496  xrlttri  10688  xaddf  10766  elfznelfzo  11147  om2uzf1oi  11248  hashnfinnn0  11598  ruclem3  12787  bitsinv1lem  12908  sadcaddlem  12924  phiprmpw  13120  iserodd  13164  fldivp1  13221  prmpwdvds  13227  vdwlem6  13309  sylow2alem2  15207  efgs1b  15323  fctop  17023  cctop  17025  ppttop  17026  iccpnfcnv  18922  iccpnfhmeo  18923  iscau2  19183  ovolicc2lem2  19367  mbfeqalem  19487  limccnp2  19732  radcnv0  20285  psercnlem1  20294  pserdvlem2  20297  logtayl  20504  cxpsqr  20547  leibpilem1  20733  rlimcnp2  20758  amgm  20782  pntpbnd1  21233  pntlem3  21256  atssma  23834  supxrnemnf  24080  xrge0iifcnv  24272  arg-ax  26070  pw2f1ocnv  26998  pm10.57  27434  afvco2  27907  elfzonelfzo  27992  con5  28317  con3ALT  28325  ax12olem3aAUX7  29163

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8