Theorem simp3lr 1029

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

Assertion

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

Proof of Theorem simp3lr

Step	Hyp	Ref	Expression
1		simplr 732	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )
2	1	3ad2ant3 980	1 |- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  f1oiso2  6039  omeu  6795  tsmsxp  18145  tgqioo  18792  ovolunlem2  19355  plyadd  20097  plymul  20098  coeeu  20105  ntrivcvgmul  25191  btwnconn1lem2  25934  btwnconn1lem3  25935  btwnconn1lem4  25936  pellex  26796  jm2.27  26977  athgt  29950  2llnjN  30061  4atlem12b  30105  lncmp  30277  cdlema2N  30286  cdleme21ct  30823  cdleme24  30846  cdleme27a  30861  cdleme28  30867  cdleme42b  30972  cdlemf  31057  dihlsscpre  31729  dihord4  31753  dihord5apre  31757

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

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938