Theorem simp11l 1172

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

Assertion

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

Proof of Theorem simp11l

Step	Hyp	Ref	Expression
1		simp1l 1085	. 2 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ph )

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  lshpsmreu  34396  exatleN  34690  2llnjaN  34852  2lplnja  34905  dalemkehl  34909  dath2  35023  pclfinN  35186  lhp2lt  35287  lhpexle3lem  35297  lhpmcvr5N  35313  lhpmcvr6N  35314  lhp2at0  35318  lhp2atnle  35319  lhp2atne  35320  lhp2at0nle  35321  lhp2at0ne  35322  4atexlemk  35333  4atexlemex6  35360  4atexlem7  35361  cdlemd2  35486  cdlemd4  35488  cdlemd7  35491  cdleme0ex2N  35511  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme11c  35548  cdleme11dN  35549  cdleme11e  35550  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15b  35562  cdleme15c  35563  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  cdleme21d  35618  cdleme21e  35619  cdleme22cN  35630  cdleme22f  35634  cdleme22f2  35635  cdleme22g  35636  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme25a  35641  cdleme25c  35643  cdleme25dN  35644  cdleme26ee  35648  cdleme26eALTN  35649  cdleme27a  35655  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme29ex  35662  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdlemefr29exN  35690  cdleme32fva  35725  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme36a  35748  cdleme37m  35750  cdleme39a  35753  cdleme42e  35767  cdleme42h  35770  cdleme42i  35771  cdleme42k  35772  cdleme43bN  35778  cdleme43dN  35780  cdleme17d2  35783  cdleme48bw  35790  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemeg46ngfr  35806  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfv  35818  cdlemf1  35849  trlord  35857  cdlemb3  35894  cdlemg7fvbwN  35895  cdlemg10a  35928  cdlemg10  35929  cdlemg12e  35935  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg17b  35950  cdlemg17g  35955  cdlemg17h  35956  cdlemg17pq  35960  cdlemg17  35965  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33c0  35990  cdlemg33a  35994  cdlemg33c  35996  cdlemg33e  35998  cdlemg35  36001  trlcone  36016  tendococl  36060  cdlemh1  36103  cdlemh2  36104  cdlemh  36105  cdlemi  36108  cdlemk5  36124  cdlemk6  36125  cdlemki  36129  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk17  36146  cdlemk1u  36147  cdlemk5u  36149  cdlemk6u  36150  cdlemkj  36151  cdlemkuv2  36155  cdlemk7u  36158  cdlemk11u  36159  cdlemk12u  36160  cdlemk26-3  36194  cdlemk37  36202  cdlemk11t  36234  cdlemk47  36237  cdlemk48  36238  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdlemk39u  36256  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  dihjatc2N  36601  dihjatc3  36602  dihmeetlem15N  36610  infleinf  39588  mullimc  39848  mullimcf  39855  limsupre  39873  addlimc  39880  limclner  39883  sge0xaddlem2  40651