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  8921  reapmul1lem  8922  reapmul1  8923  mulcanap  8993  mulcanap2  8994  divassap  9020  divdirap  9027  div11ap  9030  muldivdirap  9037  divcanap5  9044  apmul1  9118  apmul2  9119  ltdiv1  9198  ltmuldiv  9204  ledivmul  9207  lemuldiv  9211  ltdiv2  9217  lediv2  9221  ltdiv23  9222  lediv23  9223  xaddass2  10272  xlt2add  10282  modqdi  10829  expaddzap  11020  expmulzap  11022  leisorel  11289  resqrtcl  11795  xrbdtri  12042  dvdscmulr  12587  dvdsmulcr  12588  dvdsadd2b  12607  dvdsgcd  12789  rpexp12i  12933  pythagtriplem3  13046  pcpremul  13072  pceu  13074  pcqmul  13082  pcqdiv  13086  f1ocpbllem  13631  ercpbl  13652  erlecpbl  13653  cmn4  14108  ablsub4  14117  abladdsub4  14118  lidlsubcl  14824  psmetlecl  15435  xmetlecl  15468  wlkl1loop  16599