Theorem simp2l 1008

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

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

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 965

This theorem is referenced by:  simpl2l  1035  simpr2l  1041  simp12l  1095  simp22l  1101  simp32l  1107  issod  4249  funprg  5181  fsnunf  5628  f1oiso2  5736  ecopovtrn  6534  ecopovtrng  6537  addassnqg  7214  ltsonq  7230  ltanqg  7232  ltmnqg  7233  addassnq0  7294  recexprlem1ssu  7466  mulasssrg  7590  distrsrg  7591  lttrsr  7594  ltsosr  7596  ltasrg  7602  mulextsr1lem  7612  mulextsr1  7613  axmulass  7705  axdistr  7706  dmdcanap  8506  ltdiv2  8669  lediv2  8673  ltdiv23  8674  lediv23  8675  xaddass  9682  xaddass2  9683  xlt2add  9693  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  expdivap  10375  leisorel  10612  bdtrilem  11042  bdtri  11043  xrbdtri  11077  fsumsplitsnun  11220  prmexpb  11865  cnptoprest  12447  ssblps  12633  ssbl  12634  tgqioo  12755  rplogbchbase  13075