Theorem simp2l 964

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 107	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	3ad2ant2 960	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl2l  991  simpr2l  997  simp12l  1051  simp22l  1057  simp32l  1063  issod  4074  funprg  4969  fsnunf  5383  f1oiso2  5486  ecopovtrn  6226  ecopovtrng  6229  addassnqg  6572  ltsonq  6588  ltanqg  6590  ltmnqg  6591  addassnq0  6652  recexprlem1ssu  6824  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1lem  6956  mulextsr1  6957  axmulass  7039  axdistr  7040  dmdcanap  7810  ltdiv2  7965  lediv2  7969  ltdiv23  7970  lediv23  7971  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  expdivap  9527  prmexpb  10530