Theorem simp2r 1026

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

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

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 982

This theorem is referenced by:  simpl2r  1053  simpr2r  1059  simp12r  1113  simp22r  1119  simp32r  1125  issod  4350  funprg  5304  fsnunf  5758  f1oiso2  5870  tfrlemibxssdm  6380  ecopovtrn  6686  ecopovtrng  6689  dftap2  7311  addassnqg  7442  ltsonq  7458  ltanqg  7460  ltmnqg  7461  addassnq0  7522  recexprlem1ssl  7693  mulasssrg  7818  distrsrg  7819  lttrsr  7822  ltsosr  7824  ltasrg  7830  mulextsr1lem  7840  mulextsr1  7841  axmulass  7933  axdistr  7934  dmdcanap  8741  lediv2  8910  ltdiv23  8911  lediv23  8912  xaddass2  9936  xlt2add  9946  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  expdivap  10661  leisorel  10908  bdtrilem  11382  xrbdtri  11419  fldivndvdslt  12076  prmexpb  12289  pcpremul  12431  pcdiv  12440  pcqmul  12441  pcqdiv  12445  4sqlem12  12540  f1ocpbllem  12893  ercpbl  12914  erlecpbl  12915  cmn4  13375  ablsub4  13383  abladdsub4  13384  cnptoprest  14407  ssblps  14593  ssbl  14594  tgqioo  14715  plyadd  14897  plymul  14898  rplogbchbase  15082