Theorem simp3l 1049

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

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

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 1004

This theorem is referenced by:  simpl3l  1076  simpr3l  1082  simp13l  1136  simp23l  1142  simp33l  1148  issod  4414  tfisi  4683  tfrlem5  6475  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  ecopovtrn  6796  ecopovtrng  6799  dftap2  7460  addassnqg  7592  ltsonq  7608  ltanqg  7610  ltmnqg  7611  addassnq0  7672  mulasssrg  7968  distrsrg  7969  lttrsr  7972  ltsosr  7974  ltasrg  7980  mulextsr1lem  7990  mulextsr1  7991  axmulass  8083  axdistr  8084  lemul1  8763  reapmul1lem  8764  reapmul1  8765  mulcanap  8835  mulcanap2  8836  divassap  8860  divdirap  8867  div11ap  8870  muldivdirap  8877  divcanap5  8884  apmul1  8958  apmul2  8959  ltdiv1  9038  ltmuldiv  9044  ledivmul  9047  lemuldiv  9051  ltdiv2  9057  lediv2  9061  ltdiv23  9062  lediv23  9063  xaddass2  10095  xlt2add  10105  modqdi  10644  expaddzap  10835  expmulzap  10837  leisorel  11091  resqrtcl  11580  xrbdtri  11827  dvdscmulr  12371  dvdsmulcr  12372  dvdsadd2b  12391  dvdsgcd  12573  rpexp12i  12717  pythagtriplem3  12830  pcpremul  12856  pceu  12858  pcqmul  12866  pcqdiv  12870  f1ocpbllem  13383  ercpbl  13404  erlecpbl  13405  cmn4  13882  ablsub4  13890  abladdsub4  13891  lidlsubcl  14491  psmetlecl  15048  xmetlecl  15081  wlkl1loop  16155