Theorem simpr3 1000

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

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

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 975

This theorem is referenced by:  simplr3  1036  simprr3  1042  simp1r3  1090  simp2r3  1096  simp3r3  1102  3anandis  1342  isopolem  5801  tfrlemibacc  6305  tfrlemibxssdm  6306  tfrlemibfn  6307  tfr1onlembacc  6321  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembxssdm  6335  tfrcllembfn  6336  elfir  6950  prloc  7453  prmuloc2  7529  ltntri  8047  eluzuzle  9495  xlesubadd  9840  elioc2  9893  elico2  9894  elicc2  9895  fseq1p1m1  10050  seq3f1olemp  10458  seq3f1oleml  10459  bcval5  10697  hashdifpr  10755  isumss2  11356  tanaddap  11702  dvds2ln  11786  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  restopnb  12975  icnpimaex  13005  cnptopresti  13032  psmettri  13124  isxmet2d  13142  xmettri  13166  metrtri  13171  xmetres2  13173  bldisj  13195  blss2ps  13200  blss2  13201  xmstri2  13264  mstri2  13265  xmstri  13266  mstri  13267  xmstri3  13268  mstri3  13269  msrtri  13270  comet  13293  bdbl  13297  xmetxp  13301  dvconst  13455