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

Theorem anabsi7 794
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 793 . 2  |-  ( ( ps  /\  ph )  ->  ch )
32ancoms 441 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  nelrdva  3149  elunii  4044  ordelord  4632  onsucuni2  4843  fvelrn  5895  fnfi  7413  prnmax  8903  fargshiftfo  21656  monotoddzz  27044  oddcomabszz  27045  flcidc  27394  fmul01  27724  stoweidlem4  27767  stoweidlem20  27783  stoweidlem22  27785  stoweidlem27  27790  stoweidlem30  27793  stoweidlem51  27814  stoweidlem59  27822  eel2221  28902
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 179  df-an 362
  Copyright terms: Public domain W3C validator