Theorem simpr3 994

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

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

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 969

This theorem is referenced by:  simplr3  1030  simprr3  1036  simp1r3  1084  simp2r3  1090  simp3r3  1096  3anandis  1336  isopolem  5784  tfrlemibacc  6285  tfrlemibxssdm  6286  tfrlemibfn  6287  tfr1onlembacc  6301  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfrcllembacc  6314  tfrcllembxssdm  6315  tfrcllembfn  6316  elfir  6929  prloc  7423  prmuloc2  7499  ltntri  8017  eluzuzle  9465  xlesubadd  9810  elioc2  9863  elico2  9864  elicc2  9865  fseq1p1m1  10019  seq3f1olemp  10427  seq3f1oleml  10428  bcval5  10665  hashdifpr  10722  isumss2  11320  tanaddap  11666  dvds2ln  11750  divalglemeunn  11843  divalglemex  11844  divalglemeuneg  11845  restopnb  12722  icnpimaex  12752  cnptopresti  12779  psmettri  12871  isxmet2d  12889  xmettri  12913  metrtri  12918  xmetres2  12920  bldisj  12942  blss2ps  12947  blss2  12948  xmstri2  13011  mstri2  13012  xmstri  13013  mstri  13014  xmstri3  13015  mstri3  13016  msrtri  13017  comet  13040  bdbl  13044  xmetxp  13048  dvconst  13202