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  4351  funprg  5305  fsnunf  5759  f1oiso2  5871  ecopovtrn  6688  ecopovtrng  6691  dftap2  7313  addassnqg  7444  ltsonq  7460  ltanqg  7462  ltmnqg  7463  addassnq0  7524  recexprlem1ssu  7696  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1lem  7842  mulextsr1  7843  axmulass  7935  axdistr  7936  dmdcanap  8743  ltdiv2  8908  lediv2  8912  ltdiv23  8913  lediv23  8914  xaddass  9938  xaddass2  9939  xlt2add  9949  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  expdivap  10664  leisorel  10911  bdtrilem  11385  bdtri  11386  xrbdtri  11422  fsumsplitsnun  11565  prmexpb  12292  pcpremul  12434  pcdiv  12443  pcqmul  12444  pcqdiv  12448  4sqlem12  12543  f1ocpbllem  12896  ercpbl  12917  erlecpbl  12918  cmn4  13378  ablsub4  13386  abladdsub4  13387  cnptoprest  14418  ssblps  14604  ssbl  14605  tgqioo  14734  plyadd  14930  plymul  14931  rplogbchbase  15123