Theorem simpr2r 1121

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simpr2r

Step	Hyp	Ref	Expression
1		simp2r 1088	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ps )
2	1	adantl 482	1 |- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  oppccatid  16379  subccatid  16506  setccatid  16734  catccatid  16752  estrccatid  16772  xpccatid  16828  gsmsymgreqlem1  17850  kerf1hrm  18743  ax5seg  25818  3pthdlem1  27024  segconeq  32117  ifscgr  32151  brofs2  32184  brifs2  32185  idinside  32191  btwnconn1lem8  32201  btwnconn1lem11  32204  btwnconn1lem12  32205  segcon2  32212  seglecgr12im  32217  unbdqndv2  32502  lplnexllnN  34850  paddasslem9  35114  paddasslem15  35120  pmodlem2  35133  lhp2lt  35287