Theorem simp12r 1175

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1088	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ps )
2	1	3ad2ant1 1082	1 |- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta /\ et ) -> 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:  ackbij1lem16  9057  lsmcv  19141  nllyrest  21289  axcontlem4  25847  eqlkr  34386  athgt  34742  llncvrlpln2  34843  4atlem11b  34894  2lnat  35070  cdlemblem  35079  pclfinN  35186  lhp2at0nle  35321  4atexlemex6  35360  cdlemd2  35486  cdlemd8  35492  cdleme15a  35561  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme20h  35604  cdleme21c  35615  cdleme21ct  35617  cdleme22cN  35630  cdleme23b  35638  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme32le  35735  cdleme35f  35742  cdlemf1  35849  trlord  35857  cdlemg7aN  35913  cdlemg33c0  35990  trlcone  36016  cdlemg44  36021  cdlemg48  36025  cdlemky  36214  cdlemk11ta  36217  cdleml4N  36267  dihmeetlem3N  36594  dihmeetlem13N  36608  mapdpglem32  36994  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  mzpcong  37539