Theorem simp11l 1284

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

Assertion

Ref	Expression
simp11l	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Proof of Theorem simp11l

Step	Hyp	Ref	Expression
1		simp1l 1197	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1133	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  pceu  16644  maduf  21895  lshpsmreu  37427  exatleN  37723  2llnjaN  37885  2lplnja  37938  dalemkehl  37942  dath2  38056  pclfinN  38219  lhp2lt  38320  lhpexle3lem  38330  lhpmcvr5N  38346  lhpmcvr6N  38347  lhp2at0  38351  lhp2atnle  38352  lhp2atne  38353  lhp2at0nle  38354  lhp2at0ne  38355  4atexlemk  38366  4atexlemex6  38393  4atexlem7  38394  cdlemd2  38518  cdlemd4  38520  cdlemd7  38523  cdleme0ex2N  38543  cdleme7aa  38561  cdleme7c  38564  cdleme7d  38565  cdleme7e  38566  cdleme7ga  38567  cdleme7  38568  cdleme11c  38580  cdleme11dN  38581  cdleme11e  38582  cdleme11  38589  cdleme14  38592  cdleme15a  38593  cdleme15b  38594  cdleme15c  38595  cdleme15d  38596  cdleme15  38597  cdleme16b  38598  cdleme16c  38599  cdleme16d  38600  cdleme16e  38601  cdleme16f  38602  cdleme18d  38614  cdleme19b  38623  cdleme19d  38625  cdleme19e  38626  cdleme20d  38631  cdleme20e  38632  cdleme20f  38633  cdleme20g  38634  cdleme20h  38635  cdleme20j  38637  cdleme20k  38638  cdleme20l1  38639  cdleme20l2  38640  cdleme20l  38641  cdleme20m  38642  cdleme21c  38646  cdleme21ct  38648  cdleme21d  38649  cdleme21e  38650  cdleme22cN  38661  cdleme22f  38665  cdleme22f2  38666  cdleme22g  38667  cdleme23a  38668  cdleme23b  38669  cdleme23c  38670  cdleme25a  38672  cdleme25c  38674  cdleme25dN  38675  cdleme26ee  38679  cdleme26eALTN  38680  cdleme27a  38686  cdleme27N  38688  cdleme28a  38689  cdleme28b  38690  cdleme29ex  38693  cdlemefrs29bpre0  38715  cdlemefrs29cpre1  38717  cdlemefr29exN  38721  cdleme32fva  38756  cdleme32b  38761  cdleme32c  38762  cdleme32e  38764  cdleme35a  38767  cdleme35fnpq  38768  cdleme35b  38769  cdleme35c  38770  cdleme35d  38771  cdleme35e  38772  cdleme35f  38773  cdleme36a  38779  cdleme37m  38781  cdleme39a  38784  cdleme42e  38798  cdleme42h  38801  cdleme42i  38802  cdleme42k  38803  cdleme43bN  38809  cdleme43dN  38811  cdleme17d2  38814  cdleme48bw  38821  cdlemeg46c  38832  cdlemeg46nlpq  38836  cdlemeg46ngfr  38837  cdlemeg46frv  38844  cdlemeg46vrg  38846  cdlemeg46rgv  38847  cdlemeg46req  38848  cdlemeg46gfv  38849  cdlemf1  38880  trlord  38888  cdlemb3  38925  cdlemg7fvbwN  38926  cdlemg10a  38959  cdlemg10  38960  cdlemg12e  38966  cdlemg12f  38967  cdlemg12g  38968  cdlemg12  38969  cdlemg13a  38970  cdlemg13  38971  cdlemg17b  38981  cdlemg17g  38986  cdlemg17h  38987  cdlemg17pq  38991  cdlemg17  38996  cdlemg19a  39002  cdlemg19  39003  cdlemg21  39005  cdlemg27a  39011  cdlemg27b  39015  cdlemg31c  39018  cdlemg33b0  39020  cdlemg33c0  39021  cdlemg33a  39025  cdlemg33c  39027  cdlemg33e  39029  cdlemg35  39032  trlcone  39047  tendococl  39091  cdlemh1  39134  cdlemh2  39135  cdlemh  39136  cdlemi  39139  cdlemk5  39155  cdlemk6  39156  cdlemki  39160  cdlemksv2  39166  cdlemk7  39167  cdlemk11  39168  cdlemk12  39169  cdlemkole  39172  cdlemk14  39173  cdlemk15  39174  cdlemk17  39177  cdlemk1u  39178  cdlemk5u  39180  cdlemk6u  39181  cdlemkj  39182  cdlemkuv2  39186  cdlemk7u  39189  cdlemk11u  39190  cdlemk12u  39191  cdlemk26-3  39225  cdlemk37  39233  cdlemk11t  39265  cdlemk47  39268  cdlemk48  39269  cdlemk50  39271  cdlemk51  39272  cdlemk52  39273  cdlemk53a  39274  cdlemk39u  39287  dihord1  39537  dihord2a  39538  dihord2b  39539  dihord11b  39541  dihord11c  39543  dihord2pre  39544  dihord2pre2  39545  dihord5apre  39581  dihmeetlem1N  39609  dihglblem2N  39613  dihglblem3N  39614  dihglbcpreN  39619  dihmeetlem3N  39624  dihjatc1  39630  dihjatc2N  39631  dihjatc3  39632  dihmeetlem15N  39640  infleinf  43298  mullimc  43545  mullimcf  43552  limsupre  43570  addlimc  43577  limclner  43580  sge0xaddlem2  44361  itscnhlc0xyqsol  46529  itsclquadb  46540  itsclquadeu  46541