Theorem simp3l 992

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  simpl3l  1019  simpr3l  1025  simp13l  1079  simp23l  1085  simp33l  1091  issod  4201  tfisi  4461  tfrlem5  6165  tfrlemibxssdm  6178  tfr1onlembxssdm  6194  tfrcllembxssdm  6207  ecopovtrn  6480  ecopovtrng  6483  addassnqg  7138  ltsonq  7154  ltanqg  7156  ltmnqg  7157  addassnq0  7218  mulasssrg  7501  distrsrg  7502  lttrsr  7505  ltsosr  7507  ltasrg  7513  mulextsr1lem  7522  mulextsr1  7523  axmulass  7608  axdistr  7609  lemul1  8273  reapmul1lem  8274  reapmul1  8275  mulcanap  8339  mulcanap2  8340  divassap  8363  divdirap  8370  div11ap  8373  muldivdirap  8380  divcanap5  8387  apmul1  8461  apmul2  8462  ltdiv1  8536  ltmuldiv  8542  ledivmul  8545  lemuldiv  8549  ltdiv2  8555  lediv2  8559  ltdiv23  8560  lediv23  8561  xaddass2  9546  xlt2add  9556  modqdi  10058  expaddzap  10230  expmulzap  10232  leisorel  10473  resqrtcl  10693  xrbdtri  10937  dvdscmulr  11370  dvdsmulcr  11371  dvdsadd2b  11388  dvdsgcd  11546  rpexp12i  11679  psmetlecl  12323  xmetlecl  12356