Theorem simp3lr 1133

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 792	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )
2	1	3ad2ant3 1084	1 |- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> 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:  f1oiso2  6602  omeu  7665  ntrivcvgmul  14634  tsmsxp  21958  tgqioo  22603  ovolunlem2  23266  plyadd  23973  plymul  23974  coeeu  23981  tghilberti2  25533  nosupbnd1lem2  31855  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  athgt  34742  2llnjN  34853  4atlem12b  34897  lncmp  35069  cdlema2N  35078  cdleme21ct  35617  cdleme24  35640  cdleme27a  35655  cdleme28  35661  cdleme42b  35766  cdlemf  35851  dihlsscpre  36523  dihord4  36547  dihord5apre  36551  pellex  37399  jm2.27  37575