Theorem simp3l 1056

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl3l  1083  simpr3l  1089  simp13l  1143  simp23l  1149  simp33l  1155  issod  4464  tfisi  4734  tfrlem5  6585  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  ecopovtrn  6906  ecopovtrng  6909  dftap2  7618  addassnqg  7750  ltsonq  7766  ltanqg  7768  ltmnqg  7769  addassnq0  7830  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltsosr  8132  ltasrg  8138  mulextsr1lem  8148  mulextsr1  8149  axmulass  8241  axdistr  8242  lemul1  8924  reapmul1lem  8925  reapmul1  8926  mulcanap  8996  mulcanap2  8997  divassap  9023  divdirap  9030  div11ap  9033  muldivdirap  9040  divcanap5  9047  apmul1  9121  apmul2  9122  ltdiv1  9201  ltmuldiv  9207  ledivmul  9210  lemuldiv  9214  ltdiv2  9220  lediv2  9224  ltdiv23  9225  lediv23  9226  xaddass2  10283  xlt2add  10293  modqdi  10844  expaddzap  11035  expmulzap  11037  leisorel  11305  resqrtcl  11811  xrbdtri  12061  dvdscmulr  12606  dvdsmulcr  12607  dvdsadd2b  12626  dvdsgcd  12808  rpexp12i  12953  pythagtriplem3  13069  pcpremul  13095  pceu  13097  pcqmul  13105  pcqdiv  13109  f1ocpbllem  13684  ercpbl  13705  erlecpbl  13706  cmn4  14192  ablsub4  14201  abladdsub4  14202  lidlsubcl  14908  psmetlecl  15526  xmetlecl  15559  wlkl1loop  16765