Theorem simp2r 1027

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

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

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 983

This theorem is referenced by:  simpl2r  1054  simpr2r  1060  simp12r  1114  simp22r  1120  simp32r  1126  issod  4366  funprg  5324  fsnunf  5784  f1oiso2  5896  tfrlemibxssdm  6413  ecopovtrn  6719  ecopovtrng  6722  dftap2  7363  addassnqg  7495  ltsonq  7511  ltanqg  7513  ltmnqg  7514  addassnq0  7575  recexprlem1ssl  7746  mulasssrg  7871  distrsrg  7872  lttrsr  7875  ltsosr  7877  ltasrg  7883  mulextsr1lem  7893  mulextsr1  7894  axmulass  7986  axdistr  7987  dmdcanap  8795  lediv2  8964  ltdiv23  8965  lediv23  8966  xaddass2  9992  xlt2add  10002  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  expdivap  10735  leisorel  10982  swrdspsleq  11120  bdtrilem  11550  xrbdtri  11587  fldivndvdslt  12248  prmexpb  12473  pcpremul  12616  pcdiv  12625  pcqmul  12626  pcqdiv  12630  4sqlem12  12725  f1ocpbllem  13142  ercpbl  13163  erlecpbl  13164  cmn4  13641  ablsub4  13649  abladdsub4  13650  cnptoprest  14711  ssblps  14897  ssbl  14898  tgqioo  15027  plyadd  15223  plymul  15224  rplogbchbase  15422