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  4414  funprg  5377  fsnunf  5849  f1oiso2  5963  ecopovtrn  6796  ecopovtrng  6799  dftap2  7460  addassnqg  7592  ltsonq  7608  ltanqg  7610  ltmnqg  7611  addassnq0  7672  recexprlem1ssu  7844  mulasssrg  7968  distrsrg  7969  lttrsr  7972  ltsosr  7974  ltasrg  7980  mulextsr1lem  7990  mulextsr1  7991  axmulass  8083  axdistr  8084  dmdcanap  8892  ltdiv2  9057  lediv2  9061  ltdiv23  9062  lediv23  9063  xaddass  10094  xaddass2  10095  xlt2add  10105  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  expdivap  10842  leisorel  11091  swrdspsleq  11238  pfxeq  11267  ccatopth2  11288  bdtrilem  11790  bdtri  11791  xrbdtri  11827  fsumsplitsnun  11970  prmexpb  12713  pcpremul  12856  pcdiv  12865  pcqmul  12866  pcqdiv  12870  4sqlem12  12965  f1ocpbllem  13383  ercpbl  13404  erlecpbl  13405  cmn4  13882  ablsub4  13890  abladdsub4  13891  cnptoprest  14953  ssblps  15139  ssbl  15140  tgqioo  15269  plyadd  15465  plymul  15466  rplogbchbase  15664