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  4445  tfisi  4714  tfrlem5  6558  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  ecopovtrn  6879  ecopovtrng  6882  dftap2  7581  addassnqg  7713  ltsonq  7729  ltanqg  7731  ltmnqg  7732  addassnq0  7793  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  lemul1  8884  reapmul1lem  8885  reapmul1  8886  mulcanap  8956  mulcanap2  8957  divassap  8981  divdirap  8988  div11ap  8991  muldivdirap  8998  divcanap5  9005  apmul1  9079  apmul2  9080  ltdiv1  9159  ltmuldiv  9165  ledivmul  9168  lemuldiv  9172  ltdiv2  9178  lediv2  9182  ltdiv23  9183  lediv23  9184  xaddass2  10222  xlt2add  10232  modqdi  10778  expaddzap  10969  expmulzap  10971  leisorel  11234  resqrtcl  11739  xrbdtri  11986  dvdscmulr  12531  dvdsmulcr  12532  dvdsadd2b  12551  dvdsgcd  12733  rpexp12i  12877  pythagtriplem3  12990  pcpremul  13016  pceu  13018  pcqmul  13026  pcqdiv  13030  f1ocpbllem  13574  ercpbl  13595  erlecpbl  13596  cmn4  14058  ablsub4  14066  abladdsub4  14067  lidlsubcl  14761  psmetlecl  15325  xmetlecl  15358  wlkl1loop  16479