Theorem simp11r 1173

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

Assertion

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

Proof of Theorem simp11r

Step	Hyp	Ref	Expression
1		simp1r 1086	. 2 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
2	1	3ad2ant1 1082	1 |- ( ( ( ( ph /\ ps ) /\ ch /\ 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:  pceu  15551  maduf  20447  nllyrest  21289  exatleN  34690  2llnjaN  34852  2lplnja  34905  dalemceb  34924  pclfinN  35186  lhpexle3lem  35297  lhpmcvr5N  35313  lhpmcvr6N  35314  lhp2at0  35318  4atexlemw  35334  cdlemd2  35486  cdlemd4  35488  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme15a  35561  cdleme15b  35562  cdleme15d  35564  cdleme15  35565  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme18d  35582  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20d  35600  cdleme20e  35601  cdleme20f  35602  cdleme20g  35603  cdleme20h  35604  cdleme20j  35606  cdleme20k  35607  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21c  35615  cdleme21ct  35617  cdleme22cN  35630  cdleme22f  35634  cdleme22g  35636  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme25a  35641  cdleme25c  35643  cdleme25dN  35644  cdleme26ee  35648  cdleme26eALTN  35649  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme29ex  35662  cdlemefr29exN  35690  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme42h  35770  cdleme42i  35771  cdleme42k  35772  cdleme48bw  35790  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemf1  35849  trlord  35857  cdlemg7fvbwN  35895  cdlemg10  35929  cdlemg12e  35935  cdlemg12f  35936  cdlemg19a  35971  cdlemg31c  35987  cdlemg33c0  35990  cdlemg35  36001  tendococl  36060  cdlemh2  36104  cdlemh  36105  cdlemi  36108  cdlemk5  36124  cdlemk7  36136  cdlemk11  36137  cdlemk5u  36149  cdlemkj  36151  cdlemkuv2  36155  cdlemk7u  36158  cdlemk11u  36159  cdlemk26-3  36194  cdlemk11t  36234  cdlemk52  36242  cdlemk53a  36243  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord11b  36511  dihord11c  36513  dihord2pre  36514  dihord2pre2  36515  dihord5apre  36551  dihmeetlem1N  36579  dihglblem2N  36583  dihglblem3N  36584  dihglbcpreN  36589  dihmeetlem3N  36594  dihjatc1  36600  suplesup  39555  limsupre  39873  sge0xaddlem2  40651