Theorem simp2l 969

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 924

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

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  simpl2l  996  simpr2l  1002  simp12l  1056  simp22l  1062  simp32l  1068  issod  4146  funprg  5064  fsnunf  5497  f1oiso2  5606  ecopovtrn  6389  ecopovtrng  6392  addassnqg  6941  ltsonq  6957  ltanqg  6959  ltmnqg  6960  addassnq0  7021  recexprlem1ssu  7193  mulasssrg  7304  distrsrg  7305  lttrsr  7308  ltsosr  7310  ltasrg  7316  mulextsr1lem  7325  mulextsr1  7326  axmulass  7408  axdistr  7409  dmdcanap  8189  ltdiv2  8348  lediv2  8352  ltdiv23  8353  lediv23  8354  expaddzaplem  9998  expaddzap  9999  expmulzap  10001  expdivap  10006  leisorel  10242  fsumsplitsnun  10813  prmexpb  11408