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 396   ∧ 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 397  df-3an 1089

This theorem is referenced by:  pceu  16775  maduf  22134  lshpsmreu  37967  exatleN  38263  2llnjaN  38425  2lplnja  38478  dalemkehl  38482  dath2  38596  pclfinN  38759  lhp2lt  38860  lhpexle3lem  38870  lhpmcvr5N  38886  lhpmcvr6N  38887  lhp2at0  38891  lhp2atnle  38892  lhp2atne  38893  lhp2at0nle  38894  lhp2at0ne  38895  4atexlemk  38906  4atexlemex6  38933  4atexlem7  38934  cdlemd2  39058  cdlemd4  39060  cdlemd7  39063  cdleme0ex2N  39083  cdleme7aa  39101  cdleme7c  39104  cdleme7d  39105  cdleme7e  39106  cdleme7ga  39107  cdleme7  39108  cdleme11c  39120  cdleme11dN  39121  cdleme11e  39122  cdleme11  39129  cdleme14  39132  cdleme15a  39133  cdleme15b  39134  cdleme15c  39135  cdleme15d  39136  cdleme15  39137  cdleme16b  39138  cdleme16c  39139  cdleme16d  39140  cdleme16e  39141  cdleme16f  39142  cdleme18d  39154  cdleme19b  39163  cdleme19d  39165  cdleme19e  39166  cdleme20d  39171  cdleme20e  39172  cdleme20f  39173  cdleme20g  39174  cdleme20h  39175  cdleme20j  39177  cdleme20k  39178  cdleme20l1  39179  cdleme20l2  39180  cdleme20l  39181  cdleme20m  39182  cdleme21c  39186  cdleme21ct  39188  cdleme21d  39189  cdleme21e  39190  cdleme22cN  39201  cdleme22f  39205  cdleme22f2  39206  cdleme22g  39207  cdleme23a  39208  cdleme23b  39209  cdleme23c  39210  cdleme25a  39212  cdleme25c  39214  cdleme25dN  39215  cdleme26ee  39219  cdleme26eALTN  39220  cdleme27a  39226  cdleme27N  39228  cdleme28a  39229  cdleme28b  39230  cdleme29ex  39233  cdlemefrs29bpre0  39255  cdlemefrs29cpre1  39257  cdlemefr29exN  39261  cdleme32fva  39296  cdleme32b  39301  cdleme32c  39302  cdleme32e  39304  cdleme35a  39307  cdleme35fnpq  39308  cdleme35b  39309  cdleme35c  39310  cdleme35d  39311  cdleme35e  39312  cdleme35f  39313  cdleme36a  39319  cdleme37m  39321  cdleme39a  39324  cdleme42e  39338  cdleme42h  39341  cdleme42i  39342  cdleme42k  39343  cdleme43bN  39349  cdleme43dN  39351  cdleme17d2  39354  cdleme48bw  39361  cdlemeg46c  39372  cdlemeg46nlpq  39376  cdlemeg46ngfr  39377  cdlemeg46frv  39384  cdlemeg46vrg  39386  cdlemeg46rgv  39387  cdlemeg46req  39388  cdlemeg46gfv  39389  cdlemf1  39420  trlord  39428  cdlemb3  39465  cdlemg7fvbwN  39466  cdlemg10a  39499  cdlemg10  39500  cdlemg12e  39506  cdlemg12f  39507  cdlemg12g  39508  cdlemg12  39509  cdlemg13a  39510  cdlemg13  39511  cdlemg17b  39521  cdlemg17g  39526  cdlemg17h  39527  cdlemg17pq  39531  cdlemg17  39536  cdlemg19a  39542  cdlemg19  39543  cdlemg21  39545  cdlemg27a  39551  cdlemg27b  39555  cdlemg31c  39558  cdlemg33b0  39560  cdlemg33c0  39561  cdlemg33a  39565  cdlemg33c  39567  cdlemg33e  39569  cdlemg35  39572  trlcone  39587  tendococl  39631  cdlemh1  39674  cdlemh2  39675  cdlemh  39676  cdlemi  39679  cdlemk5  39695  cdlemk6  39696  cdlemki  39700  cdlemksv2  39706  cdlemk7  39707  cdlemk11  39708  cdlemk12  39709  cdlemkole  39712  cdlemk14  39713  cdlemk15  39714  cdlemk17  39717  cdlemk1u  39718  cdlemk5u  39720  cdlemk6u  39721  cdlemkj  39722  cdlemkuv2  39726  cdlemk7u  39729  cdlemk11u  39730  cdlemk12u  39731  cdlemk26-3  39765  cdlemk37  39773  cdlemk11t  39805  cdlemk47  39808  cdlemk48  39809  cdlemk50  39811  cdlemk51  39812  cdlemk52  39813  cdlemk53a  39814  cdlemk39u  39827  dihord1  40077  dihord2a  40078  dihord2b  40079  dihord11b  40081  dihord11c  40083  dihord2pre  40084  dihord2pre2  40085  dihord5apre  40121  dihmeetlem1N  40149  dihglblem2N  40153  dihglblem3N  40154  dihglbcpreN  40159  dihmeetlem3N  40164  dihjatc1  40170  dihjatc2N  40171  dihjatc3  40172  dihmeetlem15N  40180  infleinf  44068  mullimc  44318  mullimcf  44325  limsupre  44343  addlimc  44350  limclner  44353  sge0xaddlem2  45136  itscnhlc0xyqsol  47404  itsclquadb  47415  itsclquadeu  47416