Theorem simp3l 1052

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3l	|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ch /\ th ) -> ch )
2	1	3ad2ant3 1047	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl3l  1079  simpr3l  1085  simp13l  1139  simp23l  1145  simp33l  1151  issod  4440  tfisi  4709  tfrlem5  6545  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  ecopovtrn  6866  ecopovtrng  6869  dftap2  7565  addassnqg  7697  ltsonq  7713  ltanqg  7715  ltmnqg  7716  addassnq0  7777  mulasssrg  8073  distrsrg  8074  lttrsr  8077  ltsosr  8079  ltasrg  8085  mulextsr1lem  8095  mulextsr1  8096  axmulass  8188  axdistr  8189  lemul1  8867  reapmul1lem  8868  reapmul1  8869  mulcanap  8939  mulcanap2  8940  divassap  8964  divdirap  8971  div11ap  8974  muldivdirap  8981  divcanap5  8988  apmul1  9062  apmul2  9063  ltdiv1  9142  ltmuldiv  9148  ledivmul  9151  lemuldiv  9155  ltdiv2  9161  lediv2  9165  ltdiv23  9166  lediv23  9167  xaddass2  10203  xlt2add  10213  modqdi  10754  expaddzap  10945  expmulzap  10947  leisorel  11209  resqrtcl  11714  xrbdtri  11961  dvdscmulr  12506  dvdsmulcr  12507  dvdsadd2b  12526  dvdsgcd  12708  rpexp12i  12852  pythagtriplem3  12965  pcpremul  12991  pceu  12993  pcqmul  13001  pcqdiv  13005  f1ocpbllem  13523  ercpbl  13544  erlecpbl  13545  cmn4  14022  ablsub4  14030  abladdsub4  14031  lidlsubcl  14635  psmetlecl  15199  xmetlecl  15232  wlkl1loop  16353