Theorem simp2l 1047

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	3ad2ant2 1043	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

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

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 1004

This theorem is referenced by:  simpl2l  1074  simpr2l  1080  simp12l  1134  simp22l  1140  simp32l  1146  issod  4410  funprg  5371  fsnunf  5843  f1oiso2  5957  ecopovtrn  6787  ecopovtrng  6790  dftap2  7448  addassnqg  7580  ltsonq  7596  ltanqg  7598  ltmnqg  7599  addassnq0  7660  recexprlem1ssu  7832  mulasssrg  7956  distrsrg  7957  lttrsr  7960  ltsosr  7962  ltasrg  7968  mulextsr1lem  7978  mulextsr1  7979  axmulass  8071  axdistr  8072  dmdcanap  8880  ltdiv2  9045  lediv2  9049  ltdiv23  9050  lediv23  9051  xaddass  10077  xaddass2  10078  xlt2add  10088  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  expdivap  10824  leisorel  11072  swrdspsleq  11214  pfxeq  11243  ccatopth2  11264  bdtrilem  11765  bdtri  11766  xrbdtri  11802  fsumsplitsnun  11945  prmexpb  12688  pcpremul  12831  pcdiv  12840  pcqmul  12841  pcqdiv  12845  4sqlem12  12940  f1ocpbllem  13358  ercpbl  13379  erlecpbl  13380  cmn4  13857  ablsub4  13865  abladdsub4  13866  cnptoprest  14928  ssblps  15114  ssbl  15115  tgqioo  15244  plyadd  15440  plymul  15441  rplogbchbase  15639