Theorem simp2r 1009

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

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 965

This theorem is referenced by:  simpl2r  1036  simpr2r  1042  simp12r  1096  simp22r  1102  simp32r  1108  issod  4274  funprg  5213  fsnunf  5660  f1oiso2  5768  tfrlemibxssdm  6264  ecopovtrn  6566  ecopovtrng  6569  addassnqg  7281  ltsonq  7297  ltanqg  7299  ltmnqg  7300  addassnq0  7361  recexprlem1ssl  7532  mulasssrg  7657  distrsrg  7658  lttrsr  7661  ltsosr  7663  ltasrg  7669  mulextsr1lem  7679  mulextsr1  7680  axmulass  7772  axdistr  7773  dmdcanap  8574  lediv2  8741  ltdiv23  8742  lediv23  8743  xaddass2  9752  xlt2add  9762  expaddzaplem  10440  expaddzap  10441  expmulzap  10443  expdivap  10448  leisorel  10685  bdtrilem  11115  xrbdtri  11150  fldivndvdslt  11799  prmexpb  11997  cnptoprest  12586  ssblps  12772  ssbl  12773  tgqioo  12894  rplogbchbase  13214