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

Theorem anabsi5 813
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 812 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  814  anabsi8  816  3anidm12  1276  rspce  3164  onint  6506  f1oweALT  6661  php2  7596  hasheqf1oi  12223  ptcmpfi  19502  redwlk  23640  vdusgraval  23712  relexpsucl  27468  relexpcnv  27469  relexpdm  27471  relexprn  27472  rtrclreclem.trans  27482  rtrclreclem.min  27483  diophin  29249  diophun  29250  rspcegf  29883  stoweidlem36  29969
  Copyright terms: Public domain W3C validator