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  2879  onint  4586  f1oweALT  5851  php2  7046  ptcmpfi  17504  relexpsucl  23439  relexpcnv  23440  relexpdm  23443  relexprn  23444  rtrclreclem.trans  23454  rtrclreclem.min  23455  domfldref  24473  defge3  24683  istopx  24959  cmptdst  24980  limptlimpr2lem2  24987  lvsovso  25038  setiscat  25391  sgplpte21d  25548  diophin  26264  diophun  26265  rspcegf  27106
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