Theorem simp2l 1049

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

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

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 1006

This theorem is referenced by:  simpl2l  1076  simpr2l  1082  simp12l  1136  simp22l  1142  simp32l  1148  issod  4416  funprg  5380  fsnunf  5853  f1oiso2  5967  ecopovtrn  6800  ecopovtrng  6803  dftap2  7469  addassnqg  7601  ltsonq  7617  ltanqg  7619  ltmnqg  7620  addassnq0  7681  recexprlem1ssu  7853  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1lem  7999  mulextsr1  8000  axmulass  8092  axdistr  8093  dmdcanap  8901  ltdiv2  9066  lediv2  9070  ltdiv23  9071  lediv23  9072  xaddass  10103  xaddass2  10104  xlt2add  10114  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  expdivap  10851  leisorel  11100  swrdspsleq  11247  pfxeq  11276  ccatopth2  11297  bdtrilem  11799  bdtri  11800  xrbdtri  11836  fsumsplitsnun  11979  prmexpb  12722  pcpremul  12865  pcdiv  12874  pcqmul  12875  pcqdiv  12879  4sqlem12  12974  f1ocpbllem  13392  ercpbl  13413  erlecpbl  13414  cmn4  13891  ablsub4  13899  abladdsub4  13900  cnptoprest  14962  ssblps  15148  ssbl  15149  tgqioo  15278  plyadd  15474  plymul  15475  rplogbchbase  15673