Theorem simp2r 1050

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

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

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 1006

This theorem is referenced by:  simpl2r  1077  simpr2r  1083  simp12r  1137  simp22r  1143  simp32r  1149  issod  4416  funprg  5380  fsnunf  5853  f1oiso2  5967  tfrlemibxssdm  6492  ecopovtrn  6800  ecopovtrng  6803  dftap2  7469  addassnqg  7601  ltsonq  7617  ltanqg  7619  ltmnqg  7620  addassnq0  7681  recexprlem1ssl  7852  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1lem  7999  mulextsr1  8000  axmulass  8092  axdistr  8093  dmdcanap  8901  lediv2  9070  ltdiv23  9071  lediv23  9072  xaddass2  10104  xlt2add  10114  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  expdivap  10851  leisorel  11100  swrdspsleq  11247  pfxeq  11276  ccatopth2  11297  bdtrilem  11799  xrbdtri  11836  fldivndvdslt  12497  prmexpb  12722  pcpremul  12865  pcdiv  12874  pcqmul  12875  pcqdiv  12879  4sqlem12  12974  f1ocpbllem  13392  ercpbl  13413  erlecpbl  13414  cmn4  13891  ablsub4  13899  abladdsub4  13900  cnptoprest  14962  ssblps  15148  ssbl  15149  tgqioo  15278  plyadd  15474  plymul  15475  rplogbchbase  15673