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

Theorem anabsi7 792
Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi7.1  |-  ( ps 
->  ( ( ph  /\  ps )  ->  ch )
)
Assertion
Ref Expression
anabsi7  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem anabsi7
StepHypRef Expression
1 anabsi7.1 . . 3  |-  ( ps 
->  ( ( ph  /\  ps )  ->  ch )
)
21anabsi6 791 . 2  |-  ( ( ps  /\  ph )  ->  ch )
32ancoms 439 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  elunii  3832  ordelord  4414  onsucuni2  4625  fvelrn  5661  fnfi  7134  prnmax  8619  cmptdst  25568  distsava  25689  monotoddzz  27028  oddcomabszz  27029  flcidc  27379  fmul01lt1lem2  27715  climrecf  27735  stoweidlem3  27752  stoweidlem30  27779  stoweidlem42  27791  stoweidlem59  27808  eel2221  28476
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 177  df-an 360
  Copyright terms: Public domain W3C validator