Theorem simpr3 995

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 989	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	adantl 275	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simplr3  1031  simprr3  1037  simp1r3  1085  simp2r3  1091  simp3r3  1097  3anandis  1337  isopolem  5790  tfrlemibacc  6294  tfrlemibxssdm  6295  tfrlemibfn  6296  tfr1onlembacc  6310  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfrcllembacc  6323  tfrcllembxssdm  6324  tfrcllembfn  6325  elfir  6938  prloc  7432  prmuloc2  7508  ltntri  8026  eluzuzle  9474  xlesubadd  9819  elioc2  9872  elico2  9873  elicc2  9874  fseq1p1m1  10029  seq3f1olemp  10437  seq3f1oleml  10438  bcval5  10676  hashdifpr  10733  isumss2  11334  tanaddap  11680  dvds2ln  11764  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  restopnb  12821  icnpimaex  12851  cnptopresti  12878  psmettri  12970  isxmet2d  12988  xmettri  13012  metrtri  13017  xmetres2  13019  bldisj  13041  blss2ps  13046  blss2  13047  xmstri2  13110  mstri2  13111  xmstri  13112  mstri  13113  xmstri3  13114  mstri3  13115  msrtri  13116  comet  13139  bdbl  13143  xmetxp  13147  dvconst  13301