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

Theorem anabsi7 819
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 818 . 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  3295  elunii  4239  ordelord  4890  fvelrn  6009  onsucuni2  6654  fnfi  7800  prnmax  9376  monotoddzz  30854  oddcomabszz  30855  flcidc  31099  fmul01  31502  stoweidlem4  31675  stoweidlem20  31691  stoweidlem22  31693  stoweidlem27  31698  stoweidlem30  31701  stoweidlem51  31722  stoweidlem59  31730  fourierdlem21  31799  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem104  31882  eel2221  33222  syldbl2  37654
  Copyright terms: Public domain W3C validator