Theorem simp2r 1019

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

Assertion

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

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 109	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	3ad2ant2 1014	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ch )

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:  simpl2r  1046  simpr2r  1052  simp12r  1106  simp22r  1112  simp32r  1118  issod  4304  funprg  5248  fsnunf  5696  f1oiso2  5806  tfrlemibxssdm  6306  ecopovtrn  6610  ecopovtrng  6613  addassnqg  7344  ltsonq  7360  ltanqg  7362  ltmnqg  7363  addassnq0  7424  recexprlem1ssl  7595  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltsosr  7726  ltasrg  7732  mulextsr1lem  7742  mulextsr1  7743  axmulass  7835  axdistr  7836  dmdcanap  8639  lediv2  8807  ltdiv23  8808  lediv23  8809  xaddass2  9827  xlt2add  9837  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  expdivap  10527  leisorel  10772  bdtrilem  11202  xrbdtri  11239  fldivndvdslt  11894  prmexpb  12105  pcpremul  12247  pcdiv  12256  pcqmul  12257  pcqdiv  12261  cnptoprest  13033  ssblps  13219  ssbl  13220  tgqioo  13341  rplogbchbase  13662