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

Theorem anabsi5 815
Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi5.1  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
Assertion
Ref Expression
anabsi5  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem anabsi5
StepHypRef Expression
1 anabsi5.1 . . 3  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
21imp 429 . 2  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  ->  ch )
32anabss5 814 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  anabsi6  816  anabsi8  818  3anidm12  1284  rspce  3189  onint  6611  f1oweALT  6765  php2  7700  hasheqf1oi  12398  ptcmpfi  20180  redwlk  24473  vdusgraval  24772  relexpsucl  28921  relexpcnv  28922  relexpdm  28924  relexprn  28925  rtrclreclem.trans  28935  rtrclreclem.min  28936  diophin  30674  diophun  30675  rspcegf  31345  stoweidlem36  31703
  Copyright terms: Public domain W3C validator