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  4410  tfisi  4679  tfrlem5  6466  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  ecopovtrn  6787  ecopovtrng  6790  dftap2  7448  addassnqg  7580  ltsonq  7596  ltanqg  7598  ltmnqg  7599  addassnq0  7660  mulasssrg  7956  distrsrg  7957  lttrsr  7960  ltsosr  7962  ltasrg  7968  mulextsr1lem  7978  mulextsr1  7979  axmulass  8071  axdistr  8072  lemul1  8751  reapmul1lem  8752  reapmul1  8753  mulcanap  8823  mulcanap2  8824  divassap  8848  divdirap  8855  div11ap  8858  muldivdirap  8865  divcanap5  8872  apmul1  8946  apmul2  8947  ltdiv1  9026  ltmuldiv  9032  ledivmul  9035  lemuldiv  9039  ltdiv2  9045  lediv2  9049  ltdiv23  9050  lediv23  9051  xaddass2  10078  xlt2add  10088  modqdi  10626  expaddzap  10817  expmulzap  10819  leisorel  11072  resqrtcl  11555  xrbdtri  11802  dvdscmulr  12346  dvdsmulcr  12347  dvdsadd2b  12366  dvdsgcd  12548  rpexp12i  12692  pythagtriplem3  12805  pcpremul  12831  pceu  12833  pcqmul  12841  pcqdiv  12845  f1ocpbllem  13358  ercpbl  13379  erlecpbl  13380  cmn4  13857  ablsub4  13865  abladdsub4  13866  lidlsubcl  14466  psmetlecl  15023  xmetlecl  15056  wlkl1loop  16099