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  2052  pm2.61dne  2556  ordunidif  4477  tfindsg  4688  findsg  4720  dff3  5711  brtpos  6285  omwordi  6611  omass  6620  nnmwordi  6675  pssnn  7124  frfi  7147  ixpiunwdom  7350  cantnfp1lem3  7427  infxpenlem  7686  infxp  7886  ackbij1lem16  7906  pwfseqlem4a  8328  gchina  8366  prlem936  8716  supsrlem  8778  sumss  12244  fsumss  12245  ruclem2  12557  prmind2  12816  rpexp  12846  fermltl  12899  prmreclem5  13014  ramcl  13123  wunress  13254  divsfval  13498  efgsfo  15097  lt6abl  15230  gsumval3  15240  ordtrest2lem  16989  ptpjpre1  17322  fbfinnfr  17588  filufint  17667  ptcmplem2  17799  cphsqrcl3  18676  ovoliun  18917  voliunlem3  18962  volsup  18966  cxpsqr  20103  amgm  20338  wilthlem2  20360  sqff1o  20473  chtublem  20503  bposlem1  20576  bposlem3  20578  ostth  20841  atdmd  23033  atmd2  23035  mdsymlem4  23041  prodss  24450  fprodss  24451  dfon2lem9  24532  ltflcei  25312  lxflflp1  25314  nn0prpwlem  25387  dgrsub2  26487  hashunx  27294  nfsb4twAUX7  28746  nfsb4tOLD7  28895  nfsb4tw2AUXOLD7  28896  a12study6  28936  a12stdy4  28947  lplnexllnN  29571  2llnjaN  29573  paddasslem14  29840  cdleme32le  30454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator