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  4440  funprg  5406  fsnunf  5884  f1oiso2  6000  ecopovtrn  6866  ecopovtrng  6869  dftap2  7565  addassnqg  7697  ltsonq  7713  ltanqg  7715  ltmnqg  7716  addassnq0  7777  recexprlem1ssu  7949  mulasssrg  8073  distrsrg  8074  lttrsr  8077  ltsosr  8079  ltasrg  8085  mulextsr1lem  8095  mulextsr1  8096  axmulass  8188  axdistr  8189  dmdcanap  8996  ltdiv2  9161  lediv2  9165  ltdiv23  9166  lediv23  9167  xaddass  10202  xaddass2  10203  xlt2add  10213  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  expdivap  10952  leisorel  11209  swrdspsleq  11359  pfxeq  11388  ccatopth2  11409  bdtrilem  11924  bdtri  11925  xrbdtri  11961  fsumsplitsnun  12105  prmexpb  12848  pcpremul  12991  pcdiv  13000  pcqmul  13001  pcqdiv  13005  4sqlem12  13100  f1ocpbllem  13523  ercpbl  13544  erlecpbl  13545  cmn4  14022  ablsub4  14030  abladdsub4  14031  cnptoprest  15104  ssblps  15290  ssbl  15291  tgqioo  15420  plyadd  15616  plymul  15617  rplogbchbase  15815