Theorem simpr2l 1053

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

Assertion

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

Proof of Theorem simpr2l

Step	Hyp	Ref	Expression
1		simp2l 1020	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ph )
2	1	adantl 464	1 |- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ph )

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 185  df-an 369  df-3an 973

This theorem is referenced by:  oppccatid  15207  subccatid  15334  setccatid  15562  catccatid  15580  estrccatid  15600  xpccatid  15656  gsmsymgreqlem1  16654  kerf1hrm  17587  nllyidm  20156  ax5seg  24443  segconeq  29888  ifscgr  29922  brofs2  29955  brifs2  29956  idinside  29962  btwnconn1lem8  29972  btwnconn1lem12  29976  segcon2  29983  segletr  29992  outsidele  30010  lplnexllnN  35685  paddasslem9  35949  pmodlem2  35968  lhp2lt  36122  cdlemc3  36315  cdlemc4  36316  cdlemd1  36320  cdleme3b  36351  cdleme3c  36352  cdleme42ke  36608  cdlemg4c  36735