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

Theorem anabsi7 810
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 809 . 2  |-  ( ( ps  /\  ph )  ->  ch )
32ancoms 450 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:  nelrdva  3165  elunii  4093  ordelord  4737  fvelrn  5836  onsucuni2  6444  fnfi  7585  prnmax  9160  fargshiftfo  23459  monotoddzz  29209  oddcomabszz  29210  flcidc  29456  fmul01  29686  stoweidlem4  29724  stoweidlem20  29740  stoweidlem22  29742  stoweidlem27  29747  stoweidlem30  29750  stoweidlem51  29771  stoweidlem59  29779  eel2221  31259
  Copyright terms: Public domain W3C validator