Theorem simpr2 946

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 940	. 2 |- ( ( ps /\ ch /\ th ) -> ch )
2	1	adantl 271	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  simplr2  982  simprr2  988  simp1r2  1036  simp2r2  1042  simp3r2  1048  3anandis  1279  isopolem  5492  tfrlemibacc  5975  tfrlemibfn  5977  tfr1onlembacc  5991  tfr1onlembfn  5993  tfrcllembacc  6004  tfrcllembfn  6006  prltlu  6739  prdisj  6744  prmuloc2  6819  eluzuzle  8708  elioc2  9035  elico2  9036  elicc2  9037  fseq1p1m1  9187  fz0fzelfz0  9215  ibcval5  9787  dvds2ln  10373  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467