Theorem simp2l 1025

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

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

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 982

This theorem is referenced by:  simpl2l  1052  simpr2l  1058  simp12l  1112  simp22l  1118  simp32l  1124  issod  4350  funprg  5304  fsnunf  5758  f1oiso2  5870  ecopovtrn  6686  ecopovtrng  6689  dftap2  7311  addassnqg  7442  ltsonq  7458  ltanqg  7460  ltmnqg  7461  addassnq0  7522  recexprlem1ssu  7694  mulasssrg  7818  distrsrg  7819  lttrsr  7822  ltsosr  7824  ltasrg  7830  mulextsr1lem  7840  mulextsr1  7841  axmulass  7933  axdistr  7934  dmdcanap  8741  ltdiv2  8906  lediv2  8910  ltdiv23  8911  lediv23  8912  xaddass  9935  xaddass2  9936  xlt2add  9946  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  expdivap  10661  leisorel  10908  bdtrilem  11382  bdtri  11383  xrbdtri  11419  fsumsplitsnun  11562  prmexpb  12289  pcpremul  12431  pcdiv  12440  pcqmul  12441  pcqdiv  12445  4sqlem12  12540  f1ocpbllem  12893  ercpbl  12914  erlecpbl  12915  cmn4  13375  ablsub4  13383  abladdsub4  13384  cnptoprest  14407  ssblps  14593  ssbl  14594  tgqioo  14715  plyadd  14897  plymul  14898  rplogbchbase  15082