Theorem simp2l 1054

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

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

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 1011

This theorem is referenced by:  simpl2l  1081  simpr2l  1087  simp12l  1141  simp22l  1147  simp32l  1153  issod  4459  funprg  5426  fsnunf  5906  f1oiso2  6023  ecopovtrn  6896  ecopovtrng  6899  dftap2  7607  addassnqg  7739  ltsonq  7755  ltanqg  7757  ltmnqg  7758  addassnq0  7819  recexprlem1ssu  7991  mulasssrg  8115  distrsrg  8116  lttrsr  8119  ltsosr  8121  ltasrg  8127  mulextsr1lem  8137  mulextsr1  8138  axmulass  8230  axdistr  8231  dmdcanap  9042  ltdiv2  9207  lediv2  9211  ltdiv23  9212  lediv23  9213  xaddass  10250  xaddass2  10251  xlt2add  10261  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  expdivap  11005  leisorel  11267  swrdspsleq  11417  pfxeq  11446  ccatopth2  11467  bdtrilem  11983  bdtri  11984  xrbdtri  12020  fsumsplitsnun  12164  prmexpb  12907  pcpremul  13050  pcdiv  13059  pcqmul  13060  pcqdiv  13064  4sqlem12  13159  f1ocpbllem  13608  ercpbl  13629  erlecpbl  13630  cmn4  14085  ablsub4  14094  abladdsub4  14095  rng1zrlem  14233  cnptoprest  15263  ssblps  15449  ssbl  15450  tgqioo  15579  plyadd  15775  plymul  15776  rplogbchbase  15975  dichmul0or  16674