Theorem simp2r 1048

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simpl2r  1075  simpr2r  1081  simp12r  1135  simp22r  1141  simp32r  1147  issod  4410  funprg  5371  fsnunf  5843  f1oiso2  5957  tfrlemibxssdm  6479  ecopovtrn  6787  ecopovtrng  6790  dftap2  7448  addassnqg  7580  ltsonq  7596  ltanqg  7598  ltmnqg  7599  addassnq0  7660  recexprlem1ssl  7831  mulasssrg  7956  distrsrg  7957  lttrsr  7960  ltsosr  7962  ltasrg  7968  mulextsr1lem  7978  mulextsr1  7979  axmulass  8071  axdistr  8072  dmdcanap  8880  lediv2  9049  ltdiv23  9050  lediv23  9051  xaddass2  10078  xlt2add  10088  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  expdivap  10824  leisorel  11072  swrdspsleq  11215  pfxeq  11244  ccatopth2  11265  bdtrilem  11766  xrbdtri  11803  fldivndvdslt  12464  prmexpb  12689  pcpremul  12832  pcdiv  12841  pcqmul  12842  pcqdiv  12846  4sqlem12  12941  f1ocpbllem  13359  ercpbl  13380  erlecpbl  13381  cmn4  13858  ablsub4  13866  abladdsub4  13867  cnptoprest  14929  ssblps  15115  ssbl  15116  tgqioo  15245  plyadd  15441  plymul  15442  rplogbchbase  15640