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

Theorem anabsi5 791
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 419 . 2  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  ->  ch )
32anabss5 790 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anabsi6  792  anabsi8  794  3anidm12  1241  rspce  3039  onint  4767  f1oweALT  6066  php2  7284  hasheqf1oi  11627  ptcmpfi  17837  redwlk  21598  vdusgraval  21670  relexpsucl  25124  relexpcnv  25125  relexpdm  25127  relexprn  25128  rtrclreclem.trans  25138  rtrclreclem.min  25139  diophin  26812  diophun  26813  rspcegf  27651  stoweidlem36  27742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator