Theorem simp2r 1014

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

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:  simpl2r  1041  simpr2r  1047  simp12r  1101  simp22r  1107  simp32r  1113  issod  4296  funprg  5237  fsnunf  5684  f1oiso2  5794  tfrlemibxssdm  6291  ecopovtrn  6594  ecopovtrng  6597  addassnqg  7319  ltsonq  7335  ltanqg  7337  ltmnqg  7338  addassnq0  7399  recexprlem1ssl  7570  mulasssrg  7695  distrsrg  7696  lttrsr  7699  ltsosr  7701  ltasrg  7707  mulextsr1lem  7717  mulextsr1  7718  axmulass  7810  axdistr  7811  dmdcanap  8614  lediv2  8782  ltdiv23  8783  lediv23  8784  xaddass2  9802  xlt2add  9812  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  expdivap  10502  leisorel  10746  bdtrilem  11176  xrbdtri  11213  fldivndvdslt  11868  prmexpb  12079  pcpremul  12221  pcdiv  12230  pcqmul  12231  pcqdiv  12235  cnptoprest  12839  ssblps  13025  ssbl  13026  tgqioo  13147  rplogbchbase  13468