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  4409  tfisi  4678  tfrlem5  6458  tfrlemibxssdm  6471  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  ecopovtrn  6777  ecopovtrng  6780  dftap2  7433  addassnqg  7565  ltsonq  7581  ltanqg  7583  ltmnqg  7584  addassnq0  7645  mulasssrg  7941  distrsrg  7942  lttrsr  7945  ltsosr  7947  ltasrg  7953  mulextsr1lem  7963  mulextsr1  7964  axmulass  8056  axdistr  8057  lemul1  8736  reapmul1lem  8737  reapmul1  8738  mulcanap  8808  mulcanap2  8809  divassap  8833  divdirap  8840  div11ap  8843  muldivdirap  8850  divcanap5  8857  apmul1  8931  apmul2  8932  ltdiv1  9011  ltmuldiv  9017  ledivmul  9020  lemuldiv  9024  ltdiv2  9030  lediv2  9034  ltdiv23  9035  lediv23  9036  xaddass2  10062  xlt2add  10072  modqdi  10609  expaddzap  10800  expmulzap  10802  leisorel  11054  resqrtcl  11535  xrbdtri  11782  dvdscmulr  12326  dvdsmulcr  12327  dvdsadd2b  12346  dvdsgcd  12528  rpexp12i  12672  pythagtriplem3  12785  pcpremul  12811  pceu  12813  pcqmul  12821  pcqdiv  12825  f1ocpbllem  13338  ercpbl  13359  erlecpbl  13360  cmn4  13837  ablsub4  13845  abladdsub4  13846  lidlsubcl  14445  psmetlecl  15002  xmetlecl  15035