Theorem simp3l 1025

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

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

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 980

This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  issod  4319  tfisi  4586  tfrlem5  6314  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  ecopovtrn  6631  ecopovtrng  6634  dftap2  7249  addassnqg  7380  ltsonq  7396  ltanqg  7398  ltmnqg  7399  addassnq0  7460  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  lemul1  8549  reapmul1lem  8550  reapmul1  8551  mulcanap  8621  mulcanap2  8622  divassap  8646  divdirap  8653  div11ap  8656  muldivdirap  8663  divcanap5  8670  apmul1  8744  apmul2  8745  ltdiv1  8824  ltmuldiv  8830  ledivmul  8833  lemuldiv  8837  ltdiv2  8843  lediv2  8847  ltdiv23  8848  lediv23  8849  xaddass2  9869  xlt2add  9879  modqdi  10391  expaddzap  10563  expmulzap  10565  leisorel  10816  resqrtcl  11037  xrbdtri  11283  dvdscmulr  11826  dvdsmulcr  11827  dvdsadd2b  11846  dvdsgcd  12012  rpexp12i  12154  pythagtriplem3  12266  pcpremul  12292  pceu  12294  pcqmul  12302  pcqdiv  12306  f1ocpbllem  12730  ercpbl  12749  erlecpbl  12750  cmn4  13106  ablsub4  13114  abladdsub4  13115  psmetlecl  13804  xmetlecl  13837