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  7617  addassnqg  7749  ltsonq  7765  ltanqg  7767  ltmnqg  7768  addassnq0  7829  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  lemul1  8923  reapmul1lem  8924  reapmul1  8925  mulcanap  8995  mulcanap2  8996  divassap  9022  divdirap  9029  div11ap  9032  muldivdirap  9039  divcanap5  9046  apmul1  9120  apmul2  9121  ltdiv1  9200  ltmuldiv  9206  ledivmul  9209  lemuldiv  9213  ltdiv2  9219  lediv2  9223  ltdiv23  9224  lediv23  9225  xaddass2  10282  xlt2add  10292  modqdi  10842  expaddzap  11033  expmulzap  11035  leisorel  11303  resqrtcl  11809  xrbdtri  12058  dvdscmulr  12603  dvdsmulcr  12604  dvdsadd2b  12623  dvdsgcd  12805  rpexp12i  12950  pythagtriplem3  13066  pcpremul  13092  pceu  13094  pcqmul  13102  pcqdiv  13106  f1ocpbllem  13680  ercpbl  13701  erlecpbl  13702  cmn4  14157  ablsub4  14166  abladdsub4  14167  lidlsubcl  14873  psmetlecl  15484  xmetlecl  15517  wlkl1loop  16697