Theorem simp2r 1051

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

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

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 1007

This theorem is referenced by:  simpl2r  1078  simpr2r  1084  simp12r  1138  simp22r  1144  simp32r  1150  issod  4440  funprg  5406  fsnunf  5884  f1oiso2  6000  tfrlemibxssdm  6558  ecopovtrn  6866  ecopovtrng  6869  dftap2  7565  addassnqg  7697  ltsonq  7713  ltanqg  7715  ltmnqg  7716  addassnq0  7777  recexprlem1ssl  7948  mulasssrg  8073  distrsrg  8074  lttrsr  8077  ltsosr  8079  ltasrg  8085  mulextsr1lem  8095  mulextsr1  8096  axmulass  8188  axdistr  8189  dmdcanap  8996  lediv2  9165  ltdiv23  9166  lediv23  9167  xaddass2  10203  xlt2add  10213  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  expdivap  10952  leisorel  11209  swrdspsleq  11359  pfxeq  11388  ccatopth2  11409  bdtrilem  11924  xrbdtri  11961  fldivndvdslt  12623  prmexpb  12848  pcpremul  12991  pcdiv  13000  pcqmul  13001  pcqdiv  13005  4sqlem12  13100  f1ocpbllem  13523  ercpbl  13544  erlecpbl  13545  cmn4  14022  ablsub4  14030  abladdsub4  14031  cnptoprest  15104  ssblps  15290  ssbl  15291  tgqioo  15420  plyadd  15616  plymul  15617  rplogbchbase  15815