Theorem simp3r 1029

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

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

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 983

This theorem is referenced by:  simpl3r  1056  simpr3r  1062  simp13r  1116  simp23r  1122  simp33r  1128  issod  4367  tfisi  4636  fvun1  5647  f1oiso2  5898  tfrlem5  6402  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  ecopovtrn  6721  ecopovtrng  6724  dftap2  7365  addassnqg  7497  ltsonq  7513  ltanqg  7515  ltmnqg  7516  addassnq0  7577  mulasssrg  7873  distrsrg  7874  lttrsr  7877  ltsosr  7879  ltasrg  7885  mulextsr1lem  7895  mulextsr1  7896  axmulass  7988  axdistr  7989  reapmul1  8670  mulcanap  8740  mulcanap2  8741  divassap  8765  divdirap  8772  div11ap  8775  apmul1  8863  ltdiv1  8943  ltmuldiv  8949  ledivmul  8952  lemuldiv  8956  lediv2  8966  ltdiv23  8967  lediv23  8968  xaddass2  9994  xlt2add  10004  modqdi  10539  expaddzap  10730  expmulzap  10732  leisorel  10984  resqrtcl  11373  xrbdtri  11620  dvdsgcd  12366  rpexp12i  12510  pythagtriplem4  12624  pythagtriplem11  12630  pythagtriplem13  12632  pcpremul  12649  pceu  12651  pcqmul  12659  pcqdiv  12663  f1ocpbllem  13175  ercpbl  13196  erlecpbl  13197  cmn4  13674  ablsub4  13682  abladdsub4  13683  lidlsubcl  14282  psmetlecl  14839  xmetlecl  14872  xblcntrps  14918  xblcntr  14919