Theorem simp2l 1013

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	3ad2ant2 1009	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl2l  1040  simpr2l  1046  simp12l  1100  simp22l  1106  simp32l  1112  issod  4296  funprg  5237  fsnunf  5684  f1oiso2  5794  ecopovtrn  6594  ecopovtrng  6597  addassnqg  7319  ltsonq  7335  ltanqg  7337  ltmnqg  7338  addassnq0  7399  recexprlem1ssu  7571  mulasssrg  7695  distrsrg  7696  lttrsr  7699  ltsosr  7701  ltasrg  7707  mulextsr1lem  7717  mulextsr1  7718  axmulass  7810  axdistr  7811  dmdcanap  8614  ltdiv2  8778  lediv2  8782  ltdiv23  8783  lediv23  8784  xaddass  9801  xaddass2  9802  xlt2add  9812  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  expdivap  10502  leisorel  10746  bdtrilem  11176  bdtri  11177  xrbdtri  11213  fsumsplitsnun  11356  prmexpb  12079  pcpremul  12221  pcdiv  12230  pcqmul  12231  pcqdiv  12235  cnptoprest  12839  ssblps  13025  ssbl  13026  tgqioo  13147  rplogbchbase  13468