Theorem anabsi7 860

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

Step	Hyp	Ref	Expression
1		anabsi7.1	. . 3 |- ( ps -> ( ( ph /\ ps ) -> ch ) )
2	1	anabsi6 859	. 2 |- ( ( ps /\ ph ) -> ch )
3	2	ancoms 469	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  syl2an23an  1387  nelrdva  3417  elunii  4441  ordelord  5745  fvelrn  6352  onsucuni2  7034  fnfi  8238  prnmax  9817  monotoddzz  37508  oddcomabszz  37509  flcidc  37744  syldbl2  38468  fmul01  39812  fprodcnlem  39831  stoweidlem4  40221  stoweidlem20  40237  stoweidlem22  40239  stoweidlem27  40244  stoweidlem30  40247  stoweidlem51  40268  stoweidlem59  40276  fourierdlem21  40345  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem104  40427