Theorem simp3r 1053

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 110	. 2 |- ( ( ch /\ th ) -> th )
2	1	3ad2ant3 1047	1 |- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )

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

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 1007

This theorem is referenced by:  simpl3r  1080  simpr3r  1086  simp13r  1140  simp23r  1146  simp33r  1152  issod  4442  tfisi  4711  fvun1  5745  f1oiso2  6002  tfrlem5  6547  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  ecopovtrn  6868  ecopovtrng  6871  dftap2  7567  addassnqg  7699  ltsonq  7715  ltanqg  7717  ltmnqg  7718  addassnq0  7779  mulasssrg  8075  distrsrg  8076  lttrsr  8079  ltsosr  8081  ltasrg  8087  mulextsr1lem  8097  mulextsr1  8098  axmulass  8190  axdistr  8191  reapmul1  8871  mulcanap  8941  mulcanap2  8942  divassap  8966  divdirap  8973  div11ap  8976  apmul1  9064  ltdiv1  9144  ltmuldiv  9150  ledivmul  9153  lemuldiv  9157  lediv2  9167  ltdiv23  9168  lediv23  9169  xaddass2  10206  xlt2add  10216  modqdi  10758  expaddzap  10949  expmulzap  10951  leisorel  11213  resqrtcl  11718  xrbdtri  11965  dvdsgcd  12712  rpexp12i  12856  pythagtriplem4  12970  pythagtriplem11  12976  pythagtriplem13  12978  pcpremul  12995  pceu  12997  pcqmul  13005  pcqdiv  13009  f1ocpbllem  13540  ercpbl  13561  erlecpbl  13562  cmn4  14039  ablsub4  14047  abladdsub4  14048  lidlsubcl  14652  psmetlecl  15216  xmetlecl  15249  xblcntrps  15295  xblcntr  15296