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

Theorem anabsi5 814
Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi5.1  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
Assertion
Ref Expression
anabsi5  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem anabsi5
StepHypRef Expression
1 anabsi5.1 . . 3  |-  ( ph  ->  ( ( ph  /\  ps )  ->  ch )
)
21imp 429 . 2  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  ->  ch )
32anabss5 813 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:  anabsi6  815  anabsi8  817  3anidm12  1280  rspce  3202  onint  6601  f1oweALT  6758  php2  7692  hasheqf1oi  12379  ptcmpfi  20042  redwlk  24270  vdusgraval  24569  relexpsucl  28380  relexpcnv  28381  relexpdm  28383  relexprn  28384  rtrclreclem.trans  28394  rtrclreclem.min  28395  diophin  30161  diophun  30162  rspcegf  30795  stoweidlem36  31155
  Copyright terms: Public domain W3C validator