Theorem simpr1r 1119

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

Assertion

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

Proof of Theorem simpr1r

Step	Hyp	Ref	Expression
1		simp1r 1086	. 2 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
2	1	adantl 482	1 |- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ 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  dmdprdsplit  18446  neitr  20984  neitx  21410  tx1stc  21453  utop3cls  22055  metustsym  22360  3pthdlem1  27024  archiabllem1  29747  esumpcvgval  30140  esum2d  30155  ifscgr  32151  btwnconn1lem8  32201  btwnconn1lem11  32204  btwnconn1lem12  32205  segletr  32221  broutsideof3  32233  unbdqndv2  32502  lhp2lt  35287  cdlemf2  35850  cdlemn11pre  36499  stoweidlem60  40277