Theorem simpr1l 1118

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

Assertion

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

Proof of Theorem simpr1l

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

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  neiptopnei  20936  neitr  20984  neitx  21410  tx1stc  21453  utop3cls  22055  metustsym  22360  ax5seg  25818  3pthdlem1  27024  esumpcvgval  30140  esum2d  30155  ifscgr  32151  brofs2  32184  brifs2  32185  btwnconn1lem8  32201  btwnconn1lem12  32205  seglecgr12im  32217  unbdqndv2  32502  lhp2lt  35287  cdlemd1  35485  cdleme3b  35516  cdleme3c  35517  cdleme3e  35519  cdlemf2  35850  cdlemg4c  35900  cdlemn11pre  36499  dihmeetlem12N  36607  stoweidlem60  40277