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  4379  funprg  5338  fsnunf  5802  f1oiso2  5914  ecopovtrn  6737  ecopovtrng  6740  dftap2  7393  addassnqg  7525  ltsonq  7541  ltanqg  7543  ltmnqg  7544  addassnq0  7605  recexprlem1ssu  7777  mulasssrg  7901  distrsrg  7902  lttrsr  7905  ltsosr  7907  ltasrg  7913  mulextsr1lem  7923  mulextsr1  7924  axmulass  8016  axdistr  8017  dmdcanap  8825  ltdiv2  8990  lediv2  8994  ltdiv23  8995  lediv23  8996  xaddass  10021  xaddass2  10022  xlt2add  10032  expaddzaplem  10759  expaddzap  10760  expmulzap  10762  expdivap  10767  leisorel  11014  swrdspsleq  11153  pfxeq  11182  ccatopth2  11203  bdtrilem  11635  bdtri  11636  xrbdtri  11672  fsumsplitsnun  11815  prmexpb  12558  pcpremul  12701  pcdiv  12710  pcqmul  12711  pcqdiv  12715  4sqlem12  12810  f1ocpbllem  13227  ercpbl  13248  erlecpbl  13249  cmn4  13726  ablsub4  13734  abladdsub4  13735  cnptoprest  14796  ssblps  14982  ssbl  14983  tgqioo  15112  plyadd  15308  plymul  15309  rplogbchbase  15507