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 427 . 2  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  ->  ch )
32anabss5 814 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  anabsi6  816  anabsi8  818  3anidm12  1283  rspce  3202  onint  6603  f1oweALT  6757  php2  7695  hasheqf1oi  12406  rtrclreclem3  12975  rtrclreclem4  12976  ptcmpfi  20480  redwlk  24810  vdusgraval  25109  diophin  30945  diophun  30946  rspcegf  31638  stoweidlem36  32057
  Copyright terms: Public domain W3C validator