Theorem simpr1 993

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

Assertion

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

Proof of Theorem simpr1

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

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:  simplr1  1029  simprr1  1035  simp1r1  1083  simp2r1  1089  simp3r1  1095  3anandis  1337  isopolem  5789  caovlem2d  6030  tfrlemibacc  6290  tfrlemibfn  6292  tfr1onlembacc  6306  tfr1onlembfn  6308  tfrcllembacc  6319  tfrcllembfn  6321  eqsupti  6957  prmuloc2  7504  ltntri  8022  elioc2  9868  elico2  9869  elicc2  9870  fseq1p1m1  10025  elfz0ubfz0  10056  ico0  10193  seq3f1olemp  10433  seq3f1oleml  10434  bcval5  10672  isumss2  11330  tanaddap  11676  dvds2ln  11760  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  qredeq  12024  pcdvdstr  12254  isstructr  12405  icnpimaex  12811  cnptopresti  12838  upxp  12872  psmettri  12930  isxmet2d  12948  xmettri  12972  metrtri  12977  xmetres2  12979  bldisj  13001  blss2ps  13006  blss2  13007  xmstri2  13070  mstri2  13071  xmstri  13072  mstri  13073  xmstri3  13074  mstri3  13075  msrtri  13076  comet  13099  bdbl  13103  xmetxp  13107  dvconst  13261  findset  13787