Theorem simp2r 1055

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2r  1082  simpr2r  1088  simp12r  1142  simp22r  1148  simp32r  1154  issod  4466  funprg  5434  fsnunf  5918  f1oiso2  6036  tfrlemibxssdm  6603  ecopovtrn  6911  ecopovtrng  6914  dftap2  7623  addassnqg  7755  ltsonq  7771  ltanqg  7773  ltmnqg  7774  addassnq0  7835  recexprlem1ssl  8006  mulasssrg  8131  distrsrg  8132  lttrsr  8135  ltsosr  8137  ltasrg  8143  mulextsr1lem  8153  mulextsr1  8154  axmulass  8246  axdistr  8247  dmdcanap  9060  lediv2  9229  ltdiv23  9230  lediv23  9231  xaddass2  10288  xlt2add  10298  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  expdivap  11047  leisorel  11310  swrdspsleq  11460  pfxeq  11489  ccatopth2  11510  bdtrilem  12029  xrbdtri  12066  fldivndvdslt  12728  prmexpb  12954  pcpremul  13100  pcdiv  13109  pcqmul  13110  pcqdiv  13114  4sqlem12  13209  f1ocpbllem  13689  ercpbl  13710  erlecpbl  13711  cmn4  14197  ablsub4  14206  abladdsub4  14207  mvrf1fi  15219  cnptoprest  15482  ssblps  15668  ssbl  15669  tgqioo  15798  plyadd  15994  plymul  15995  rplogbchbase  16203  dichmul0or  16982