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  4337  tfisi  4604  tfrlem5  6340  tfrlemibxssdm  6353  tfr1onlembxssdm  6369  tfrcllembxssdm  6382  ecopovtrn  6659  ecopovtrng  6662  dftap2  7281  addassnqg  7412  ltsonq  7428  ltanqg  7430  ltmnqg  7431  addassnq0  7492  mulasssrg  7788  distrsrg  7789  lttrsr  7792  ltsosr  7794  ltasrg  7800  mulextsr1lem  7810  mulextsr1  7811  axmulass  7903  axdistr  7904  lemul1  8581  reapmul1lem  8582  reapmul1  8583  mulcanap  8653  mulcanap2  8654  divassap  8678  divdirap  8685  div11ap  8688  muldivdirap  8695  divcanap5  8702  apmul1  8776  apmul2  8777  ltdiv1  8856  ltmuldiv  8862  ledivmul  8865  lemuldiv  8869  ltdiv2  8875  lediv2  8879  ltdiv23  8880  lediv23  8881  xaddass2  9902  xlt2add  9912  modqdi  10425  expaddzap  10598  expmulzap  10600  leisorel  10852  resqrtcl  11073  xrbdtri  11319  dvdscmulr  11862  dvdsmulcr  11863  dvdsadd2b  11882  dvdsgcd  12048  rpexp12i  12190  pythagtriplem3  12302  pcpremul  12328  pceu  12330  pcqmul  12338  pcqdiv  12342  f1ocpbllem  12790  ercpbl  12810  erlecpbl  12811  cmn4  13261  ablsub4  13269  abladdsub4  13270  lidlsubcl  13820  psmetlecl  14311  xmetlecl  14344