Theorem simp3l 1028

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

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

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 983

This theorem is referenced by:  simpl3l  1055  simpr3l  1061  simp13l  1115  simp23l  1121  simp33l  1127  issod  4374  tfisi  4643  tfrlem5  6413  tfrlemibxssdm  6426  tfr1onlembxssdm  6442  tfrcllembxssdm  6455  ecopovtrn  6732  ecopovtrng  6735  dftap2  7383  addassnqg  7515  ltsonq  7531  ltanqg  7533  ltmnqg  7534  addassnq0  7595  mulasssrg  7891  distrsrg  7892  lttrsr  7895  ltsosr  7897  ltasrg  7903  mulextsr1lem  7913  mulextsr1  7914  axmulass  8006  axdistr  8007  lemul1  8686  reapmul1lem  8687  reapmul1  8688  mulcanap  8758  mulcanap2  8759  divassap  8783  divdirap  8790  div11ap  8793  muldivdirap  8800  divcanap5  8807  apmul1  8881  apmul2  8882  ltdiv1  8961  ltmuldiv  8967  ledivmul  8970  lemuldiv  8974  ltdiv2  8980  lediv2  8984  ltdiv23  8985  lediv23  8986  xaddass2  10012  xlt2add  10022  modqdi  10559  expaddzap  10750  expmulzap  10752  leisorel  11004  resqrtcl  11415  xrbdtri  11662  dvdscmulr  12206  dvdsmulcr  12207  dvdsadd2b  12226  dvdsgcd  12408  rpexp12i  12552  pythagtriplem3  12665  pcpremul  12691  pceu  12693  pcqmul  12701  pcqdiv  12705  f1ocpbllem  13217  ercpbl  13238  erlecpbl  13239  cmn4  13716  ablsub4  13724  abladdsub4  13725  lidlsubcl  14324  psmetlecl  14881  xmetlecl  14914