Theorem simp3l 1025

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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 980

This theorem is referenced by:  simpl3l  1052  simpr3l  1058  simp13l  1112  simp23l  1118  simp33l  1124  issod  4313  tfisi  4580  tfrlem5  6305  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  ecopovtrn  6622  ecopovtrng  6625  addassnqg  7356  ltsonq  7372  ltanqg  7374  ltmnqg  7375  addassnq0  7436  mulasssrg  7732  distrsrg  7733  lttrsr  7736  ltsosr  7738  ltasrg  7744  mulextsr1lem  7754  mulextsr1  7755  axmulass  7847  axdistr  7848  lemul1  8524  reapmul1lem  8525  reapmul1  8526  mulcanap  8595  mulcanap2  8596  divassap  8620  divdirap  8627  div11ap  8630  muldivdirap  8637  divcanap5  8644  apmul1  8718  apmul2  8719  ltdiv1  8798  ltmuldiv  8804  ledivmul  8807  lemuldiv  8811  ltdiv2  8817  lediv2  8821  ltdiv23  8822  lediv23  8823  xaddass2  9841  xlt2add  9851  modqdi  10362  expaddzap  10534  expmulzap  10536  leisorel  10785  resqrtcl  11006  xrbdtri  11252  dvdscmulr  11795  dvdsmulcr  11796  dvdsadd2b  11815  dvdsgcd  11980  rpexp12i  12122  pythagtriplem3  12234  pcpremul  12260  pceu  12262  pcqmul  12270  pcqdiv  12274  cmn4  12907  ablsub4  12915  abladdsub4  12916  psmetlecl  13405  xmetlecl  13438