Theorem simp3l 1027

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

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

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 982

This theorem is referenced by:  simpl3l  1054  simpr3l  1060  simp13l  1114  simp23l  1120  simp33l  1126  issod  4364  tfisi  4633  tfrlem5  6390  tfrlemibxssdm  6403  tfr1onlembxssdm  6419  tfrcllembxssdm  6432  ecopovtrn  6709  ecopovtrng  6712  dftap2  7345  addassnqg  7477  ltsonq  7493  ltanqg  7495  ltmnqg  7496  addassnq0  7557  mulasssrg  7853  distrsrg  7854  lttrsr  7857  ltsosr  7859  ltasrg  7865  mulextsr1lem  7875  mulextsr1  7876  axmulass  7968  axdistr  7969  lemul1  8648  reapmul1lem  8649  reapmul1  8650  mulcanap  8720  mulcanap2  8721  divassap  8745  divdirap  8752  div11ap  8755  muldivdirap  8762  divcanap5  8769  apmul1  8843  apmul2  8844  ltdiv1  8923  ltmuldiv  8929  ledivmul  8932  lemuldiv  8936  ltdiv2  8942  lediv2  8946  ltdiv23  8947  lediv23  8948  xaddass2  9974  xlt2add  9984  modqdi  10518  expaddzap  10709  expmulzap  10711  leisorel  10963  resqrtcl  11259  xrbdtri  11506  dvdscmulr  12050  dvdsmulcr  12051  dvdsadd2b  12070  dvdsgcd  12252  rpexp12i  12396  pythagtriplem3  12509  pcpremul  12535  pceu  12537  pcqmul  12545  pcqdiv  12549  f1ocpbllem  13060  ercpbl  13081  erlecpbl  13082  cmn4  13559  ablsub4  13567  abladdsub4  13568  lidlsubcl  14167  psmetlecl  14724  xmetlecl  14757