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

Theorem pm2.43a 45
Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43a.1  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
pm2.43a  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem pm2.43a
StepHypRef Expression
1 id 19 . 2  |-  ( ps 
->  ps )
2 pm2.43a.1 . 2  |-  ( ps 
->  ( ph  ->  ( ps  ->  ch ) ) )
31, 2mpid 37 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  pm2.43b  46  rspc  2878  intss1  3877  fvopab3ig  5599  odi  6577  nndi  6621  inf3lem2  7330  pr2ne  7635  zorn2lem7  8129  uzind2  10104  uzindOLD  10106  sqlecan  11209  clatlem  14216  fiinopn  16647  dvrunz  21100  eqfnung2  25118  supwlub  25274  dfps2  25289  rltrooo  25415  osneisi  25531  limptlimpr2lem1  25574  limptlimpr2lem2  25575  bwt2  25592  icccon4  25702  intvconlem1  25703  propsrc  25868  tartarmap  25888  fnctartar  25907  fnctartar2  25908  domcatfun  25925  indcls2  25996  clscnc  26010  iscol3  26094  isibg1a6  26125  bsstrs  26146  nbssntrs  26147  pdiveql  26168  ee223  28406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator