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 )

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:  simpl2l  1081  simpr2l  1087  simp12l  1141  simp22l  1147  simp32l  1153  issod  4466  funprg  5434  fsnunf  5918  f1oiso2  6036  ecopovtrn  6910  ecopovtrng  6913  dftap2  7623  addassnqg  7755  ltsonq  7771  ltanqg  7773  ltmnqg  7774  addassnq0  7835  recexprlem1ssu  8007  mulasssrg  8131  distrsrg  8132  lttrsr  8135  ltsosr  8137  ltasrg  8143  mulextsr1lem  8153  mulextsr1  8154  axmulass  8246  axdistr  8247  dmdcanap  9060  ltdiv2  9225  lediv2  9229  ltdiv23  9230  lediv23  9231  xaddass  10288  xaddass2  10289  xlt2add  10299  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  expdivap  11048  leisorel  11311  swrdspsleq  11461  pfxeq  11490  ccatopth2  11511  bdtrilem  12030  bdtri  12031  xrbdtri  12067  fsumsplitsnun  12211  prmexpb  12955  pcpremul  13101  pcdiv  13110  pcqmul  13111  pcqdiv  13115  4sqlem12  13210  f1ocpbllem  13690  ercpbl  13711  erlecpbl  13712  cmn4  14198  ablsub4  14207  abladdsub4  14208  rng1zrlem  14365  cnptoprest  15465  ssblps  15651  ssbl  15652  tgqioo  15781  plyadd  15977  plymul  15978  rplogbchbase  16186  dichmul0or  16965