Theorem simp2l 1047

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

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

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 1004

This theorem is referenced by:  simpl2l  1074  simpr2l  1080  simp12l  1134  simp22l  1140  simp32l  1146  issod  4409  funprg  5370  fsnunf  5838  f1oiso2  5950  ecopovtrn  6777  ecopovtrng  6780  dftap2  7433  addassnqg  7565  ltsonq  7581  ltanqg  7583  ltmnqg  7584  addassnq0  7645  recexprlem1ssu  7817  mulasssrg  7941  distrsrg  7942  lttrsr  7945  ltsosr  7947  ltasrg  7953  mulextsr1lem  7963  mulextsr1  7964  axmulass  8056  axdistr  8057  dmdcanap  8865  ltdiv2  9030  lediv2  9034  ltdiv23  9035  lediv23  9036  xaddass  10061  xaddass2  10062  xlt2add  10072  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  expdivap  10807  leisorel  11054  swrdspsleq  11194  pfxeq  11223  ccatopth2  11244  bdtrilem  11745  bdtri  11746  xrbdtri  11782  fsumsplitsnun  11925  prmexpb  12668  pcpremul  12811  pcdiv  12820  pcqmul  12821  pcqdiv  12825  4sqlem12  12920  f1ocpbllem  13338  ercpbl  13359  erlecpbl  13360  cmn4  13837  ablsub4  13845  abladdsub4  13846  cnptoprest  14907  ssblps  15093  ssbl  15094  tgqioo  15223  plyadd  15419  plymul  15420  rplogbchbase  15618