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

Theorem anabsi7 816
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 815 . 2  |-  ( ( ps  /\  ph )  ->  ch )
32ancoms 453 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  3306  elunii  4243  ordelord  4893  fvelrn  6008  onsucuni2  6640  fnfi  7787  prnmax  9362  fargshiftfo  24300  monotoddzz  30470  oddcomabszz  30471  flcidc  30717  fmul01  31085  stoweidlem4  31259  stoweidlem20  31275  stoweidlem22  31277  stoweidlem27  31282  stoweidlem30  31285  stoweidlem51  31306  stoweidlem59  31314  eel2221  32444
  Copyright terms: Public domain W3C validator