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  4466  tfisi  4736  tfrlem5  6590  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  ecopovtrn  6911  ecopovtrng  6914  dftap2  7623  addassnqg  7755  ltsonq  7771  ltanqg  7773  ltmnqg  7774  addassnq0  7835  mulasssrg  8131  distrsrg  8132  lttrsr  8135  ltsosr  8137  ltasrg  8143  mulextsr1lem  8153  mulextsr1  8154  axmulass  8246  axdistr  8247  lemul1  8929  reapmul1lem  8930  reapmul1  8931  mulcanap  9001  mulcanap2  9002  divassap  9028  divdirap  9035  div11ap  9038  muldivdirap  9045  divcanap5  9052  apmul1  9126  apmul2  9127  ltdiv1  9206  ltmuldiv  9212  ledivmul  9215  lemuldiv  9219  ltdiv2  9225  lediv2  9229  ltdiv23  9230  lediv23  9231  xaddass2  10288  xlt2add  10298  modqdi  10849  expaddzap  11040  expmulzap  11042  leisorel  11310  resqrtcl  11816  xrbdtri  12066  dvdscmulr  12611  dvdsmulcr  12612  dvdsadd2b  12631  dvdsgcd  12813  rpexp12i  12958  pythagtriplem3  13074  pcpremul  13100  pceu  13102  pcqmul  13110  pcqdiv  13114  f1ocpbllem  13689  ercpbl  13710  erlecpbl  13711  cmn4  14197  ablsub4  14206  abladdsub4  14207  lidlsubcl  14932  psmetlecl  15577  xmetlecl  15610  wlkl1loop  16821