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

Theorem pm2.61d 150
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
StepHypRef Expression
1 pm2.61d.2 . . . 4  |-  ( ph  ->  ( -.  ps  ->  ch ) )
21con1d 116 . . 3  |-  ( ph  ->  ( -.  ch  ->  ps ) )
3 pm2.61d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3syld 40 . 2  |-  ( ph  ->  ( -.  ch  ->  ch ) )
54pm2.18d 103 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61d1  151  pm2.61d2  152  pm5.21ndd  343  bija  344  pm2.61dan  766  ecase3d  909  nfsb4t  2020  pm2.61dne  2523  ordunidif  4440  tfindsg  4651  findsg  4683  dff3  5673  brtpos  6243  omwordi  6569  omass  6578  nnmwordi  6633  pssnn  7081  frfi  7102  ixpiunwdom  7305  cantnfp1lem3  7382  infxpenlem  7641  infxp  7841  ackbij1lem16  7861  pwfseqlem4a  8283  gchina  8321  prlem936  8671  supsrlem  8733  sumss  12197  fsumss  12198  ruclem2  12510  prmind2  12769  rpexp  12799  fermltl  12852  prmreclem5  12967  ramcl  13076  wunress  13207  divsfval  13449  efgsfo  15048  lt6abl  15181  gsumval3  15191  ordtrest2lem  16933  ptpjpre1  17266  fbfinnfr  17536  filufint  17615  ptcmplem2  17747  cphsqrcl3  18623  ovoliun  18864  voliunlem3  18909  volsup  18913  cxpsqr  20050  amgm  20285  wilthlem2  20307  sqff1o  20420  chtublem  20450  bposlem1  20523  bposlem3  20525  ostth  20788  atdmd  22978  atmd2  22980  mdsymlem4  22986  dfon2lem9  24147  nn0prpwlem  26238  dgrsub2  27339  a12study6  29118  a12stdy4  29129  lplnexllnN  29753  2llnjaN  29755  paddasslem14  30022  cdleme32le  30636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator