Theorem simp2r 991

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

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

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  simpl2r  1018  simpr2r  1024  simp12r  1078  simp22r  1084  simp32r  1090  issod  4201  funprg  5131  fsnunf  5574  f1oiso2  5682  tfrlemibxssdm  6178  ecopovtrn  6480  ecopovtrng  6483  addassnqg  7138  ltsonq  7154  ltanqg  7156  ltmnqg  7157  addassnq0  7218  recexprlem1ssl  7389  mulasssrg  7501  distrsrg  7502  lttrsr  7505  ltsosr  7507  ltasrg  7513  mulextsr1lem  7522  mulextsr1  7523  axmulass  7608  axdistr  7609  dmdcanap  8395  lediv2  8559  ltdiv23  8560  lediv23  8561  xaddass2  9546  xlt2add  9556  expaddzaplem  10229  expaddzap  10230  expmulzap  10232  expdivap  10237  leisorel  10473  bdtrilem  10902  xrbdtri  10937  fldivndvdslt  11480  prmexpb  11675  cnptoprest  12250  ssblps  12414  ssbl  12415  tgqioo  12533