Theorem simp2l 1025

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

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

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 982

This theorem is referenced by:  simpl2l  1052  simpr2l  1058  simp12l  1112  simp22l  1118  simp32l  1124  issod  4365  funprg  5323  fsnunf  5783  f1oiso2  5895  ecopovtrn  6718  ecopovtrng  6721  dftap2  7362  addassnqg  7494  ltsonq  7510  ltanqg  7512  ltmnqg  7513  addassnq0  7574  recexprlem1ssu  7746  mulasssrg  7870  distrsrg  7871  lttrsr  7874  ltsosr  7876  ltasrg  7882  mulextsr1lem  7892  mulextsr1  7893  axmulass  7985  axdistr  7986  dmdcanap  8794  ltdiv2  8959  lediv2  8963  ltdiv23  8964  lediv23  8965  xaddass  9990  xaddass2  9991  xlt2add  10001  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  expdivap  10733  leisorel  10980  bdtrilem  11492  bdtri  11493  xrbdtri  11529  fsumsplitsnun  11672  prmexpb  12415  pcpremul  12558  pcdiv  12567  pcqmul  12568  pcqdiv  12572  4sqlem12  12667  f1ocpbllem  13084  ercpbl  13105  erlecpbl  13106  cmn4  13583  ablsub4  13591  abladdsub4  13592  cnptoprest  14653  ssblps  14839  ssbl  14840  tgqioo  14969  plyadd  15165  plymul  15166  rplogbchbase  15364