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

Theorem anabsi7 826
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 825 . 2  |-  ( ( ps  /\  ph )  ->  ch )
32ancoms 454 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  nelrdva  3281  elunii  4221  ordelord  5461  fvelrn  6027  onsucuni2  6672  fnfi  7852  prnmax  9421  monotoddzz  35711  oddcomabszz  35712  flcidc  35960  syldbl2  36469  eel2221  36941  fmul01  37478  stoweidlem4  37684  stoweidlem20  37700  stoweidlem22  37702  stoweidlem27  37707  stoweidlem30  37711  stoweidlem51  37732  stoweidlem59  37740  fourierdlem21  37810  fourierdlem89  37879  fourierdlem90  37880  fourierdlem91  37881  fourierdlem104  37894
  Copyright terms: Public domain W3C validator