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

Theorem pm2.61d 152
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 118 . . 3  |-  ( ph  ->  ( -.  ch  ->  ps ) )
3 pm2.61d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3syld 42 . 2  |-  ( ph  ->  ( -.  ch  ->  ch ) )
54pm2.18d 105 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61d1  153  pm2.61d2  154  pm5.21ndd  344  bija  345  pm2.61dan  767  ecase3d  910  ax10lem2  1989  nfsb4t  2129  pm2.61dne  2644  ordunidif  4589  tfindsg  4799  findsg  4831  dff3  5841  brtpos  6447  omwordi  6773  omass  6782  nnmwordi  6837  pssnn  7286  frfi  7311  ixpiunwdom  7515  cantnfp1lem3  7592  infxpenlem  7851  infxp  8051  ackbij1lem16  8071  pwfseqlem4a  8492  gchina  8530  prlem936  8880  supsrlem  8942  hashunx  11615  sumss  12473  fsumss  12474  ruclem2  12786  prmind2  13045  rpexp  13075  fermltl  13128  prmreclem5  13243  ramcl  13352  wunress  13483  divsfval  13727  efgsfo  15326  lt6abl  15459  gsumval3  15469  ordtrest2lem  17221  ptpjpre1  17556  fbfinnfr  17826  filufint  17905  ptcmplem2  18037  cphsqrcl3  19103  ovoliun  19354  voliunlem3  19399  volsup  19403  cxpsqr  20547  amgm  20782  wilthlem2  20805  sqff1o  20918  chtublem  20948  bposlem1  21021  bposlem3  21023  ostth  21286  atdmd  23854  atmd2  23856  mdsymlem4  23862  prodss  25226  fprodss  25227  dfon2lem9  25361  ltflcei  26140  lxflflp1  26142  nn0prpwlem  26215  dgrsub2  27207  nfsb4twAUX7  29280  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  lplnexllnN  30046  2llnjaN  30048  paddasslem14  30315  cdleme32le  30929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator