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

Theorem pm2.61d 153
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 119 . . 3  |-  ( ph  ->  ( -.  ch  ->  ps ) )
3 pm2.61d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3syld 43 . 2  |-  ( ph  ->  ( -.  ch  ->  ch ) )
54pm2.18d 106 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61d1  154  pm2.61d2  155  pm5.21ndd  345  bija  346  pm2.61dan  768  ecase3d  911  ax10lem2  2024  nfsb4tOLD  2130  pm2.61dne  2683  ordunidif  4631  tfindsg  4842  findsg  4874  dff3  5884  brtpos  6490  omwordi  6816  omass  6825  nnmwordi  6880  pssnn  7329  frfi  7354  ixpiunwdom  7561  cantnfp1lem3  7638  infxpenlem  7897  infxp  8097  ackbij1lem16  8117  pwfseqlem4a  8538  gchina  8576  prlem936  8926  supsrlem  8988  hashunx  11662  sumss  12520  fsumss  12521  ruclem2  12833  prmind2  13092  rpexp  13122  fermltl  13175  prmreclem5  13290  ramcl  13399  wunress  13530  divsfval  13774  efgsfo  15373  lt6abl  15506  gsumval3  15516  ordtrest2lem  17269  ptpjpre1  17605  fbfinnfr  17875  filufint  17954  ptcmplem2  18086  cphsqrcl3  19152  ovoliun  19403  voliunlem3  19448  volsup  19452  cxpsqr  20596  amgm  20831  wilthlem2  20854  sqff1o  20967  chtublem  20997  bposlem1  21070  bposlem3  21072  ostth  21335  atdmd  23903  atmd2  23905  mdsymlem4  23911  prodss  25275  fprodss  25276  dfon2lem9  25420  ltflcei  26241  lxflflp1  26243  nn0prpwlem  26327  dgrsub2  27318  swrdccat3blem  28240  nfsb4twAUX7  29638  nfsb4tOLD7  29807  nfsb4tw2AUXOLD7  29808  lplnexllnN  30423  2llnjaN  30425  paddasslem14  30692  cdleme32le  31306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator