Theorem simp3l 1051

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

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

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 1006

This theorem is referenced by:  simpl3l  1078  simpr3l  1084  simp13l  1138  simp23l  1144  simp33l  1150  issod  4416  tfisi  4685  tfrlem5  6479  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  ecopovtrn  6800  ecopovtrng  6803  dftap2  7469  addassnqg  7601  ltsonq  7617  ltanqg  7619  ltmnqg  7620  addassnq0  7681  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltsosr  7983  ltasrg  7989  mulextsr1lem  7999  mulextsr1  8000  axmulass  8092  axdistr  8093  lemul1  8772  reapmul1lem  8773  reapmul1  8774  mulcanap  8844  mulcanap2  8845  divassap  8869  divdirap  8876  div11ap  8879  muldivdirap  8886  divcanap5  8893  apmul1  8967  apmul2  8968  ltdiv1  9047  ltmuldiv  9053  ledivmul  9056  lemuldiv  9060  ltdiv2  9066  lediv2  9070  ltdiv23  9071  lediv23  9072  xaddass2  10104  xlt2add  10114  modqdi  10653  expaddzap  10844  expmulzap  10846  leisorel  11100  resqrtcl  11589  xrbdtri  11836  dvdscmulr  12380  dvdsmulcr  12381  dvdsadd2b  12400  dvdsgcd  12582  rpexp12i  12726  pythagtriplem3  12839  pcpremul  12865  pceu  12867  pcqmul  12875  pcqdiv  12879  f1ocpbllem  13392  ercpbl  13413  erlecpbl  13414  cmn4  13891  ablsub4  13899  abladdsub4  13900  lidlsubcl  14500  psmetlecl  15057  xmetlecl  15090  wlkl1loop  16208