Theorem simpr3 957

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 951	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	adantl 273	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

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

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

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

This theorem is referenced by:  simplr3  993  simprr3  999  simp1r3  1047  simp2r3  1053  simp3r3  1059  3anandis  1293  isopolem  5655  tfrlemibacc  6153  tfrlemibxssdm  6154  tfrlemibfn  6155  tfr1onlembacc  6169  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfrcllembacc  6182  tfrcllembxssdm  6183  tfrcllembfn  6184  prloc  7200  prmuloc2  7276  ltntri  7761  eluzuzle  9184  xlesubadd  9507  elioc2  9560  elico2  9561  elicc2  9562  fseq1p1m1  9715  seq3f1olemp  10116  seq3f1oleml  10117  bcval5  10350  hashdifpr  10407  isumss2  11001  tanaddap  11244  dvds2ln  11321  divalglemeunn  11413  divalglemex  11414  divalglemeuneg  11415  restopnb  12132  icnpimaex  12161  cnptopresti  12188  psmettri  12258  isxmet2d  12276  xmettri  12300  metrtri  12305  xmetres2  12307  bldisj  12329  blss2ps  12334  blss2  12335  xmstri2  12398  mstri2  12399  xmstri  12400  mstri  12401  xmstri3  12402  mstri3  12403  msrtri  12404  comet  12427  bdbl  12431  dvconst  12534