Theorem simp3l 1025

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

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

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 980

This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  issod  4320  tfisi  4587  tfrlem5  6315  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  ecopovtrn  6632  ecopovtrng  6635  dftap2  7250  addassnqg  7381  ltsonq  7397  ltanqg  7399  ltmnqg  7400  addassnq0  7461  mulasssrg  7757  distrsrg  7758  lttrsr  7761  ltsosr  7763  ltasrg  7769  mulextsr1lem  7779  mulextsr1  7780  axmulass  7872  axdistr  7873  lemul1  8550  reapmul1lem  8551  reapmul1  8552  mulcanap  8622  mulcanap2  8623  divassap  8647  divdirap  8654  div11ap  8657  muldivdirap  8664  divcanap5  8671  apmul1  8745  apmul2  8746  ltdiv1  8825  ltmuldiv  8831  ledivmul  8834  lemuldiv  8838  ltdiv2  8844  lediv2  8848  ltdiv23  8849  lediv23  8850  xaddass2  9870  xlt2add  9880  modqdi  10392  expaddzap  10564  expmulzap  10566  leisorel  10817  resqrtcl  11038  xrbdtri  11284  dvdscmulr  11827  dvdsmulcr  11828  dvdsadd2b  11847  dvdsgcd  12013  rpexp12i  12155  pythagtriplem3  12267  pcpremul  12293  pceu  12295  pcqmul  12303  pcqdiv  12307  f1ocpbllem  12731  ercpbl  12750  erlecpbl  12751  cmn4  13108  ablsub4  13116  abladdsub4  13117  psmetlecl  13837  xmetlecl  13870