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  3934  ordelord  4517  onsucuni2  4728  fvelrn  5768  fnfi  7281  prnmax  8766  nelrdva  23379  ustref  23721  monotoddzz  26534  oddcomabszz  26535  flcidc  26885  fmul01lt1lem2  27221  climrecf  27241  stoweidlem3  27258  stoweidlem30  27285  stoweidlem42  27297  stoweidlem59  27314  fargshiftfo  27763  eel2221  28229
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