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  4366  tfisi  4635  fvun1  5645  f1oiso2  5896  tfrlem5  6400  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  ecopovtrn  6719  ecopovtrng  6722  dftap2  7363  addassnqg  7495  ltsonq  7511  ltanqg  7513  ltmnqg  7514  addassnq0  7575  mulasssrg  7871  distrsrg  7872  lttrsr  7875  ltsosr  7877  ltasrg  7883  mulextsr1lem  7893  mulextsr1  7894  axmulass  7986  axdistr  7987  reapmul1  8668  mulcanap  8738  mulcanap2  8739  divassap  8763  divdirap  8770  div11ap  8773  apmul1  8861  ltdiv1  8941  ltmuldiv  8947  ledivmul  8950  lemuldiv  8954  lediv2  8964  ltdiv23  8965  lediv23  8966  xaddass2  9992  xlt2add  10002  modqdi  10537  expaddzap  10728  expmulzap  10730  leisorel  10982  resqrtcl  11340  xrbdtri  11587  dvdsgcd  12333  rpexp12i  12477  pythagtriplem4  12591  pythagtriplem11  12597  pythagtriplem13  12599  pcpremul  12616  pceu  12618  pcqmul  12626  pcqdiv  12630  f1ocpbllem  13142  ercpbl  13163  erlecpbl  13164  cmn4  13641  ablsub4  13649  abladdsub4  13650  lidlsubcl  14249  psmetlecl  14806  xmetlecl  14839  xblcntrps  14885  xblcntr  14886