Theorem simp2l 1007

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	3ad2ant2 1003	1 |- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpl2l  1034  simpr2l  1040  simp12l  1094  simp22l  1100  simp32l  1106  issod  4241  funprg  5173  fsnunf  5620  f1oiso2  5728  ecopovtrn  6526  ecopovtrng  6529  addassnqg  7190  ltsonq  7206  ltanqg  7208  ltmnqg  7209  addassnq0  7270  recexprlem1ssu  7442  mulasssrg  7566  distrsrg  7567  lttrsr  7570  ltsosr  7572  ltasrg  7578  mulextsr1lem  7588  mulextsr1  7589  axmulass  7681  axdistr  7682  dmdcanap  8482  ltdiv2  8645  lediv2  8649  ltdiv23  8650  lediv23  8651  xaddass  9652  xaddass2  9653  xlt2add  9663  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  expdivap  10344  leisorel  10580  bdtrilem  11010  bdtri  11011  xrbdtri  11045  fsumsplitsnun  11188  prmexpb  11829  cnptoprest  12408  ssblps  12594  ssbl  12595  tgqioo  12716