Theorem simp11l 1286

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  pceu  16399  maduf  21538  lshpsmreu  36860  exatleN  37155  2llnjaN  37317  2lplnja  37370  dalemkehl  37374  dath2  37488  pclfinN  37651  lhp2lt  37752  lhpexle3lem  37762  lhpmcvr5N  37778  lhpmcvr6N  37779  lhp2at0  37783  lhp2atnle  37784  lhp2atne  37785  lhp2at0nle  37786  lhp2at0ne  37787  4atexlemk  37798  4atexlemex6  37825  4atexlem7  37826  cdlemd2  37950  cdlemd4  37952  cdlemd7  37955  cdleme0ex2N  37975  cdleme7aa  37993  cdleme7c  37996  cdleme7d  37997  cdleme7e  37998  cdleme7ga  37999  cdleme7  38000  cdleme11c  38012  cdleme11dN  38013  cdleme11e  38014  cdleme11  38021  cdleme14  38024  cdleme15a  38025  cdleme15b  38026  cdleme15c  38027  cdleme15d  38028  cdleme15  38029  cdleme16b  38030  cdleme16c  38031  cdleme16d  38032  cdleme16e  38033  cdleme16f  38034  cdleme18d  38046  cdleme19b  38055  cdleme19d  38057  cdleme19e  38058  cdleme20d  38063  cdleme20e  38064  cdleme20f  38065  cdleme20g  38066  cdleme20h  38067  cdleme20j  38069  cdleme20k  38070  cdleme20l1  38071  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21c  38078  cdleme21ct  38080  cdleme21d  38081  cdleme21e  38082  cdleme22cN  38093  cdleme22f  38097  cdleme22f2  38098  cdleme22g  38099  cdleme23a  38100  cdleme23b  38101  cdleme23c  38102  cdleme25a  38104  cdleme25c  38106  cdleme25dN  38107  cdleme26ee  38111  cdleme26eALTN  38112  cdleme27a  38118  cdleme27N  38120  cdleme28a  38121  cdleme28b  38122  cdleme29ex  38125  cdlemefrs29bpre0  38147  cdlemefrs29cpre1  38149  cdlemefr29exN  38153  cdleme32fva  38188  cdleme32b  38193  cdleme32c  38194  cdleme32e  38196  cdleme35a  38199  cdleme35fnpq  38200  cdleme35b  38201  cdleme35c  38202  cdleme35d  38203  cdleme35e  38204  cdleme35f  38205  cdleme36a  38211  cdleme37m  38213  cdleme39a  38216  cdleme42e  38230  cdleme42h  38233  cdleme42i  38234  cdleme42k  38235  cdleme43bN  38241  cdleme43dN  38243  cdleme17d2  38246  cdleme48bw  38253  cdlemeg46c  38264  cdlemeg46nlpq  38268  cdlemeg46ngfr  38269  cdlemeg46frv  38276  cdlemeg46vrg  38278  cdlemeg46rgv  38279  cdlemeg46req  38280  cdlemeg46gfv  38281  cdlemf1  38312  trlord  38320  cdlemb3  38357  cdlemg7fvbwN  38358  cdlemg10a  38391  cdlemg10  38392  cdlemg12e  38398  cdlemg12f  38399  cdlemg12g  38400  cdlemg12  38401  cdlemg13a  38402  cdlemg13  38403  cdlemg17b  38413  cdlemg17g  38418  cdlemg17h  38419  cdlemg17pq  38423  cdlemg17  38428  cdlemg19a  38434  cdlemg19  38435  cdlemg21  38437  cdlemg27a  38443  cdlemg27b  38447  cdlemg31c  38450  cdlemg33b0  38452  cdlemg33c0  38453  cdlemg33a  38457  cdlemg33c  38459  cdlemg33e  38461  cdlemg35  38464  trlcone  38479  tendococl  38523  cdlemh1  38566  cdlemh2  38567  cdlemh  38568  cdlemi  38571  cdlemk5  38587  cdlemk6  38588  cdlemki  38592  cdlemksv2  38598  cdlemk7  38599  cdlemk11  38600  cdlemk12  38601  cdlemkole  38604  cdlemk14  38605  cdlemk15  38606  cdlemk17  38609  cdlemk1u  38610  cdlemk5u  38612  cdlemk6u  38613  cdlemkj  38614  cdlemkuv2  38618  cdlemk7u  38621  cdlemk11u  38622  cdlemk12u  38623  cdlemk26-3  38657  cdlemk37  38665  cdlemk11t  38697  cdlemk47  38700  cdlemk48  38701  cdlemk50  38703  cdlemk51  38704  cdlemk52  38705  cdlemk53a  38706  cdlemk39u  38719  dihord1  38969  dihord2a  38970  dihord2b  38971  dihord11b  38973  dihord11c  38975  dihord2pre  38976  dihord2pre2  38977  dihord5apre  39013  dihmeetlem1N  39041  dihglblem2N  39045  dihglblem3N  39046  dihglbcpreN  39051  dihmeetlem3N  39056  dihjatc1  39062  dihjatc2N  39063  dihjatc3  39064  dihmeetlem15N  39072  infleinf  42584  mullimc  42832  mullimcf  42839  limsupre  42857  addlimc  42864  limclner  42867  sge0xaddlem2  43647  itscnhlc0xyqsol  45784  itsclquadb  45795  itsclquadeu  45796