Theorem simp3lr 1030

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 733	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )
2	1	3ad2ant3 981	1 |- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 360   /\ w3a 937

This theorem is referenced by:  f1oiso2  6075  omeu  6831  tsmsxp  18189  tgqioo  18836  ovolunlem2  19399  plyadd  20141  plymul  20142  coeeu  20149  ntrivcvgmul  25235  btwnconn1lem2  26027  btwnconn1lem3  26028  btwnconn1lem4  26029  pellex  26912  jm2.27  27093  athgt  30327  2llnjN  30438  4atlem12b  30482  lncmp  30654  cdlema2N  30663  cdleme21ct  31200  cdleme24  31223  cdleme27a  31238  cdleme28  31244  cdleme42b  31349  cdlemf  31434  dihlsscpre  32106  dihord4  32130  dihord5apre  32134

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 179  df-an 362  df-3an 939