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

Theorem anabsi5 790
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 418 . 2  |-  ( (
ph  /\  ( ph  /\ 
ps ) )  ->  ch )
32anabss5 789 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anabsi6  791  anabsi8  793  3anidm12  1239  rspce  2892  onint  4602  f1oweALT  5867  php2  7062  ptcmpfi  17520  relexpsucl  24043  relexpcnv  24044  relexpdm  24047  relexprn  24048  rtrclreclem.trans  24058  rtrclreclem.min  24059  domfldref  25164  defge3  25374  istopx  25650  cmptdst  25671  limptlimpr2lem2  25678  lvsovso  25729  setiscat  26082  sgplpte21d  26239  diophin  26955  diophun  26956  rspcegf  27797  redwlk  28364
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator