Theorem simp2l 1018

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 1014	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

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

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 975

This theorem is referenced by:  simpl2l  1045  simpr2l  1051  simp12l  1105  simp22l  1111  simp32l  1117  issod  4304  funprg  5248  fsnunf  5696  f1oiso2  5806  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  ltsonq  7360  ltanqg  7362  ltmnqg  7363  addassnq0  7424  recexprlem1ssu  7596  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  dmdcanap  8639  ltdiv2  8803  lediv2  8807  ltdiv23  8808  lediv23  8809  xaddass  9826  xaddass2  9827  xlt2add  9837  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  expdivap  10527  leisorel  10772  bdtrilem  11202  bdtri  11203  xrbdtri  11239  fsumsplitsnun  11382  prmexpb  12105  pcpremul  12247  pcdiv  12256  pcqmul  12257  pcqdiv  12261  cnptoprest  13033  ssblps  13219  ssbl  13220  tgqioo  13341  rplogbchbase  13662