Theorem simp3l 1027

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

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

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 982

This theorem is referenced by:  simpl3l  1054  simpr3l  1060  simp13l  1114  simp23l  1120  simp33l  1126  issod  4365  tfisi  4634  tfrlem5  6399  tfrlemibxssdm  6412  tfr1onlembxssdm  6428  tfrcllembxssdm  6441  ecopovtrn  6718  ecopovtrng  6721  dftap2  7362  addassnqg  7494  ltsonq  7510  ltanqg  7512  ltmnqg  7513  addassnq0  7574  mulasssrg  7870  distrsrg  7871  lttrsr  7874  ltsosr  7876  ltasrg  7882  mulextsr1lem  7892  mulextsr1  7893  axmulass  7985  axdistr  7986  lemul1  8665  reapmul1lem  8666  reapmul1  8667  mulcanap  8737  mulcanap2  8738  divassap  8762  divdirap  8769  div11ap  8772  muldivdirap  8779  divcanap5  8786  apmul1  8860  apmul2  8861  ltdiv1  8940  ltmuldiv  8946  ledivmul  8949  lemuldiv  8953  ltdiv2  8959  lediv2  8963  ltdiv23  8964  lediv23  8965  xaddass2  9991  xlt2add  10001  modqdi  10535  expaddzap  10726  expmulzap  10728  leisorel  10980  resqrtcl  11311  xrbdtri  11558  dvdscmulr  12102  dvdsmulcr  12103  dvdsadd2b  12122  dvdsgcd  12304  rpexp12i  12448  pythagtriplem3  12561  pcpremul  12587  pceu  12589  pcqmul  12597  pcqdiv  12601  f1ocpbllem  13113  ercpbl  13134  erlecpbl  13135  cmn4  13612  ablsub4  13620  abladdsub4  13621  lidlsubcl  14220  psmetlecl  14777  xmetlecl  14810