Theorem simp2l 1050

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

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

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 1007

This theorem is referenced by:  simpl2l  1077  simpr2l  1083  simp12l  1137  simp22l  1143  simp32l  1149  issod  4422  funprg  5387  fsnunf  5862  f1oiso2  5978  ecopovtrn  6844  ecopovtrng  6847  dftap2  7513  addassnqg  7645  ltsonq  7661  ltanqg  7663  ltmnqg  7664  addassnq0  7725  recexprlem1ssu  7897  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1lem  8043  mulextsr1  8044  axmulass  8136  axdistr  8137  dmdcanap  8944  ltdiv2  9109  lediv2  9113  ltdiv23  9114  lediv23  9115  xaddass  10148  xaddass2  10149  xlt2add  10159  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  expdivap  10898  leisorel  11147  swrdspsleq  11297  pfxeq  11326  ccatopth2  11347  bdtrilem  11862  bdtri  11863  xrbdtri  11899  fsumsplitsnun  12043  prmexpb  12786  pcpremul  12929  pcdiv  12938  pcqmul  12939  pcqdiv  12943  4sqlem12  13038  f1ocpbllem  13456  ercpbl  13477  erlecpbl  13478  cmn4  13955  ablsub4  13963  abladdsub4  13964  cnptoprest  15033  ssblps  15219  ssbl  15220  tgqioo  15349  plyadd  15545  plymul  15546  rplogbchbase  15744