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  4354  tfisi  4623  tfrlem5  6372  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  ecopovtrn  6691  ecopovtrng  6694  dftap2  7318  addassnqg  7449  ltsonq  7465  ltanqg  7467  ltmnqg  7468  addassnq0  7529  mulasssrg  7825  distrsrg  7826  lttrsr  7829  ltsosr  7831  ltasrg  7837  mulextsr1lem  7847  mulextsr1  7848  axmulass  7940  axdistr  7941  lemul1  8620  reapmul1lem  8621  reapmul1  8622  mulcanap  8692  mulcanap2  8693  divassap  8717  divdirap  8724  div11ap  8727  muldivdirap  8734  divcanap5  8741  apmul1  8815  apmul2  8816  ltdiv1  8895  ltmuldiv  8901  ledivmul  8904  lemuldiv  8908  ltdiv2  8914  lediv2  8918  ltdiv23  8919  lediv23  8920  xaddass2  9945  xlt2add  9955  modqdi  10484  expaddzap  10675  expmulzap  10677  leisorel  10929  resqrtcl  11194  xrbdtri  11441  dvdscmulr  11985  dvdsmulcr  11986  dvdsadd2b  12005  dvdsgcd  12179  rpexp12i  12323  pythagtriplem3  12436  pcpremul  12462  pceu  12464  pcqmul  12472  pcqdiv  12476  f1ocpbllem  12953  ercpbl  12974  erlecpbl  12975  cmn4  13435  ablsub4  13443  abladdsub4  13444  lidlsubcl  14043  psmetlecl  14570  xmetlecl  14603