Theorem pm2.61d 170

Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61d.1	|- ( ph -> ( ps -> ch ) )
pm2.61d.2	|- ( ph -> ( -. ps -> ch ) )

Assertion

Ref	Expression
pm2.61d	|- ( ph -> ch )

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.2	. . . 4 |- ( ph -> ( -. ps -> ch ) )
2	1	con1d 139	. . 3 |- ( ph -> ( -. ch -> ps ) )
3		pm2.61d.1	. . 3 |- ( ph -> ( ps -> ch ) )
4	2, 3	syld 47	. 2 |- ( ph -> ( -. ch -> ch ) )
5	4	pm2.18d 124	1 |- ( ph -> ch )

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:  pm2.61d1  171  pm2.61d2  172  pm5.21ndd  369  bija  370  pm2.61dan  832  ecase3d  984  axc11nlemOLD2  1988  axc11nlemOLD  2160  axc11nlemALT  2306  pm2.61dne  2880  ordunidif  5773  dff3  6372  tfindsg  7060  findsg  7093  brtpos  7361  omwordi  7651  omass  7660  nnmwordi  7715  pssnn  8178  frfi  8205  ixpiunwdom  8496  cantnfp1lem3  8577  infxpenlem  8836  infxp  9037  ackbij1lem16  9057  axpowndlem3  9421  pwfseqlem4a  9483  gchina  9521  prlem936  9869  supsrlem  9932  flflp1  12608  hashunx  13175  swrdccat3blem  13495  repswswrd  13531  sumss  14455  fsumss  14456  prodss  14677  fprodss  14678  ruclem2  14961  prmind2  15398  rpexp  15432  fermltl  15489  prmreclem5  15624  ramcl  15733  wunress  15940  divsfval  16207  efgsfo  18152  lt6abl  18296  gsumval3  18308  mdetunilem8  20425  ordtrest2lem  21007  ptpjpre1  21374  fbfinnfr  21645  filufint  21724  ptcmplem2  21857  cphsqrtcl3  22987  ovoliun  23273  voliunlem3  23320  volsup  23324  cxpsqrt  24449  amgm  24717  wilthlem2  24795  sqff1o  24908  chtublem  24936  bposlem1  25009  bposlem3  25011  ostth  25328  clwwisshclwwslemlem  26926  atdmd  29257  atmd2  29259  mdsymlem4  29265  ordtrest2NEWlem  29968  eulerpartlemb  30430  dfon2lem9  31696  nosupbnd1lem1  31854  nn0prpwlem  32317  ltflcei  33397  poimirlem30  33439  lplnexllnN  34850  2llnjaN  34852  paddasslem14  35119  cdleme32le  35735  dgrsub2  37705  iccelpart  41369  lighneallem3  41524  lighneal  41528