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  11521  bdtri  11522  xrbdtri  11558  fsumsplitsnun  11701  prmexpb  12444  pcpremul  12587  pcdiv  12596  pcqmul  12597  pcqdiv  12601  4sqlem12  12696  f1ocpbllem  13113  ercpbl  13134  erlecpbl  13135  cmn4  13612  ablsub4  13620  abladdsub4  13621  cnptoprest  14682  ssblps  14868  ssbl  14869  tgqioo  14998  plyadd  15194  plymul  15195  rplogbchbase  15393