Theorem simp3l 1052

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

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

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 1007

This theorem is referenced by:  simpl3l  1079  simpr3l  1085  simp13l  1139  simp23l  1145  simp33l  1151  issod  4422  tfisi  4691  tfrlem5  6523  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  ecopovtrn  6844  ecopovtrng  6847  dftap2  7513  addassnqg  7645  ltsonq  7661  ltanqg  7663  ltmnqg  7664  addassnq0  7725  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltsosr  8027  ltasrg  8033  mulextsr1lem  8043  mulextsr1  8044  axmulass  8136  axdistr  8137  lemul1  8815  reapmul1lem  8816  reapmul1  8817  mulcanap  8887  mulcanap2  8888  divassap  8912  divdirap  8919  div11ap  8922  muldivdirap  8929  divcanap5  8936  apmul1  9010  apmul2  9011  ltdiv1  9090  ltmuldiv  9096  ledivmul  9099  lemuldiv  9103  ltdiv2  9109  lediv2  9113  ltdiv23  9114  lediv23  9115  xaddass2  10149  xlt2add  10159  modqdi  10700  expaddzap  10891  expmulzap  10893  leisorel  11147  resqrtcl  11652  xrbdtri  11899  dvdscmulr  12444  dvdsmulcr  12445  dvdsadd2b  12464  dvdsgcd  12646  rpexp12i  12790  pythagtriplem3  12903  pcpremul  12929  pceu  12931  pcqmul  12939  pcqdiv  12943  f1ocpbllem  13456  ercpbl  13477  erlecpbl  13478  cmn4  13955  ablsub4  13963  abladdsub4  13964  lidlsubcl  14566  psmetlecl  15128  xmetlecl  15161  wlkl1loop  16282