Theorem simp3l 1015

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 108	. 2 |- ( ( ch /\ th ) -> ch )
2	1	3ad2ant3 1010	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )

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

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 970

This theorem is referenced by:  simpl3l  1042  simpr3l  1048  simp13l  1102  simp23l  1108  simp33l  1114  issod  4297  tfisi  4564  tfrlem5  6282  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  ecopovtrn  6598  ecopovtrng  6601  addassnqg  7323  ltsonq  7339  ltanqg  7341  ltmnqg  7342  addassnq0  7403  mulasssrg  7699  distrsrg  7700  lttrsr  7703  ltsosr  7705  ltasrg  7711  mulextsr1lem  7721  mulextsr1  7722  axmulass  7814  axdistr  7815  lemul1  8491  reapmul1lem  8492  reapmul1  8493  mulcanap  8562  mulcanap2  8563  divassap  8586  divdirap  8593  div11ap  8596  muldivdirap  8603  divcanap5  8610  apmul1  8684  apmul2  8685  ltdiv1  8763  ltmuldiv  8769  ledivmul  8772  lemuldiv  8776  ltdiv2  8782  lediv2  8786  ltdiv23  8787  lediv23  8788  xaddass2  9806  xlt2add  9816  modqdi  10327  expaddzap  10499  expmulzap  10501  leisorel  10750  resqrtcl  10971  xrbdtri  11217  dvdscmulr  11760  dvdsmulcr  11761  dvdsadd2b  11780  dvdsgcd  11945  rpexp12i  12087  pythagtriplem3  12199  pcpremul  12225  pceu  12227  pcqmul  12235  pcqdiv  12239  psmetlecl  12974  xmetlecl  13007