Theorem simp3r 932

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3r	|- ((ph /\ ps /\ (ch /\ th)) -> th)

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 103	. 2 |- ((ch /\ th) -> th)
2	1	3ad2ant3 926	1 |- ((ph /\ ps /\ (ch /\ th)) -> th)

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  simpl3r  959  simpr3r  965  simp13r  1019  simp23r  1025  simp33r  1031  issod  4047  tfisi  4253  fvun1  5182  f1oiso2  5409  tfrlem5  5871  ecopovtrn  6139  ecopovtrng  6142  addassnqg  6366  ltsonq  6382  ltanqg  6384  ltmnqg  6385  addassnq0  6445  mulasssrg  6686  distrsrg  6687  lttrsr  6690  ltsosr  6692  ltasrg  6698  mulextsr1lem  6706  mulextsr1  6707  axmulass  6757  axdistr  6758  reapmul1  7379  mulcanap  7428  mulcanap2  7429  divassap  7451  divdirap  7456  div11ap  7459  apmul1  7546  ltdiv1  7615  ltmuldiv  7621  ledivmul  7624  lemuldiv  7628  lediv2  7638  ltdiv23  7639  lediv23  7640  expaddzap  8953  expmulzap  8955