Theorem simp3l 1056

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

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

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 1011

This theorem is referenced by:  simpl3l  1083  simpr3l  1089  simp13l  1143  simp23l  1149  simp33l  1155  issod  4459  tfisi  4729  tfrlem5  6575  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  ecopovtrn  6896  ecopovtrng  6899  dftap2  7607  addassnqg  7739  ltsonq  7755  ltanqg  7757  ltmnqg  7758  addassnq0  7819  mulasssrg  8115  distrsrg  8116  lttrsr  8119  ltsosr  8121  ltasrg  8127  mulextsr1lem  8137  mulextsr1  8138  axmulass  8230  axdistr  8231  lemul1  8911  reapmul1lem  8912  reapmul1  8913  mulcanap  8983  mulcanap2  8984  divassap  9010  divdirap  9017  div11ap  9020  muldivdirap  9027  divcanap5  9034  apmul1  9108  apmul2  9109  ltdiv1  9188  ltmuldiv  9194  ledivmul  9197  lemuldiv  9201  ltdiv2  9207  lediv2  9211  ltdiv23  9212  lediv23  9213  xaddass2  10251  xlt2add  10261  modqdi  10807  expaddzap  10998  expmulzap  11000  leisorel  11267  resqrtcl  11773  xrbdtri  12020  dvdscmulr  12565  dvdsmulcr  12566  dvdsadd2b  12585  dvdsgcd  12767  rpexp12i  12911  pythagtriplem3  13024  pcpremul  13050  pceu  13052  pcqmul  13060  pcqdiv  13064  f1ocpbllem  13608  ercpbl  13629  erlecpbl  13630  cmn4  14085  ablsub4  14094  abladdsub4  14095  lidlsubcl  14796  psmetlecl  15358  xmetlecl  15391  wlkl1loop  16513