Theorem simp2l 970

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

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

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

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

This theorem is referenced by:  simpl2l  997  simpr2l  1003  simp12l  1057  simp22l  1063  simp32l  1069  issod  4157  funprg  5079  fsnunf  5513  f1oiso2  5622  ecopovtrn  6405  ecopovtrng  6408  addassnqg  7004  ltsonq  7020  ltanqg  7022  ltmnqg  7023  addassnq0  7084  recexprlem1ssu  7256  mulasssrg  7367  distrsrg  7368  lttrsr  7371  ltsosr  7373  ltasrg  7379  mulextsr1lem  7388  mulextsr1  7389  axmulass  7471  axdistr  7472  dmdcanap  8252  ltdiv2  8411  lediv2  8415  ltdiv23  8416  lediv23  8417  expaddzaplem  10061  expaddzap  10062  expmulzap  10064  expdivap  10069  leisorel  10305  fsumsplitsnun  10876  prmexpb  11471