Theorem simp2l 1026

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

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

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 983

This theorem is referenced by:  simpl2l  1053  simpr2l  1059  simp12l  1113  simp22l  1119  simp32l  1125  issod  4366  funprg  5324  fsnunf  5784  f1oiso2  5896  ecopovtrn  6719  ecopovtrng  6722  dftap2  7363  addassnqg  7495  ltsonq  7511  ltanqg  7513  ltmnqg  7514  addassnq0  7575  recexprlem1ssu  7747  mulasssrg  7871  distrsrg  7872  lttrsr  7875  ltsosr  7877  ltasrg  7883  mulextsr1lem  7893  mulextsr1  7894  axmulass  7986  axdistr  7987  dmdcanap  8795  ltdiv2  8960  lediv2  8964  ltdiv23  8965  lediv23  8966  xaddass  9991  xaddass2  9992  xlt2add  10002  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  expdivap  10735  leisorel  10982  swrdspsleq  11120  bdtrilem  11550  bdtri  11551  xrbdtri  11587  fsumsplitsnun  11730  prmexpb  12473  pcpremul  12616  pcdiv  12625  pcqmul  12626  pcqdiv  12630  4sqlem12  12725  f1ocpbllem  13142  ercpbl  13163  erlecpbl  13164  cmn4  13641  ablsub4  13649  abladdsub4  13650  cnptoprest  14711  ssblps  14897  ssbl  14898  tgqioo  15027  plyadd  15223  plymul  15224  rplogbchbase  15422