Theorem simp11l 1285

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  pceu  16774  maduf  22585  lshpsmreu  39365  exatleN  39660  2llnjaN  39822  2lplnja  39875  dalemkehl  39879  dath2  39993  pclfinN  40156  lhp2lt  40257  lhpexle3lem  40267  lhpmcvr5N  40283  lhpmcvr6N  40284  lhp2at0  40288  lhp2atnle  40289  lhp2atne  40290  lhp2at0nle  40291  lhp2at0ne  40292  4atexlemk  40303  4atexlemex6  40330  4atexlem7  40331  cdlemd2  40455  cdlemd4  40457  cdlemd7  40460  cdleme0ex2N  40480  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11c  40517  cdleme11dN  40518  cdleme11e  40519  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15b  40531  cdleme15c  40532  cdleme15d  40533  cdleme15  40534  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme18d  40551  cdleme19b  40560  cdleme19d  40562  cdleme19e  40563  cdleme20d  40568  cdleme20e  40569  cdleme20f  40570  cdleme20g  40571  cdleme20h  40572  cdleme20j  40574  cdleme20k  40575  cdleme20l1  40576  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21c  40583  cdleme21ct  40585  cdleme21d  40586  cdleme21e  40587  cdleme22cN  40598  cdleme22f  40602  cdleme22f2  40603  cdleme22g  40604  cdleme23a  40605  cdleme23b  40606  cdleme23c  40607  cdleme25a  40609  cdleme25c  40611  cdleme25dN  40612  cdleme26ee  40616  cdleme26eALTN  40617  cdleme27a  40623  cdleme27N  40625  cdleme28a  40626  cdleme28b  40627  cdleme29ex  40630  cdlemefrs29bpre0  40652  cdlemefrs29cpre1  40654  cdlemefr29exN  40658  cdleme32fva  40693  cdleme32b  40698  cdleme32c  40699  cdleme32e  40701  cdleme35a  40704  cdleme35fnpq  40705  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35e  40709  cdleme35f  40710  cdleme36a  40716  cdleme37m  40718  cdleme39a  40721  cdleme42e  40735  cdleme42h  40738  cdleme42i  40739  cdleme42k  40740  cdleme43bN  40746  cdleme43dN  40748  cdleme17d2  40751  cdleme48bw  40758  cdlemeg46c  40769  cdlemeg46nlpq  40773  cdlemeg46ngfr  40774  cdlemeg46frv  40781  cdlemeg46vrg  40783  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemeg46gfv  40786  cdlemf1  40817  trlord  40825  cdlemb3  40862  cdlemg7fvbwN  40863  cdlemg10a  40896  cdlemg10  40897  cdlemg12e  40903  cdlemg12f  40904  cdlemg12g  40905  cdlemg12  40906  cdlemg13a  40907  cdlemg13  40908  cdlemg17b  40918  cdlemg17g  40923  cdlemg17h  40924  cdlemg17pq  40928  cdlemg17  40933  cdlemg19a  40939  cdlemg19  40940  cdlemg21  40942  cdlemg27a  40948  cdlemg27b  40952  cdlemg31c  40955  cdlemg33b0  40957  cdlemg33c0  40958  cdlemg33a  40962  cdlemg33c  40964  cdlemg33e  40966  cdlemg35  40969  trlcone  40984  tendococl  41028  cdlemh1  41071  cdlemh2  41072  cdlemh  41073  cdlemi  41076  cdlemk5  41092  cdlemk6  41093  cdlemki  41097  cdlemksv2  41103  cdlemk7  41104  cdlemk11  41105  cdlemk12  41106  cdlemkole  41109  cdlemk14  41110  cdlemk15  41111  cdlemk17  41114  cdlemk1u  41115  cdlemk5u  41117  cdlemk6u  41118  cdlemkj  41119  cdlemkuv2  41123  cdlemk7u  41126  cdlemk11u  41127  cdlemk12u  41128  cdlemk26-3  41162  cdlemk37  41170  cdlemk11t  41202  cdlemk47  41205  cdlemk48  41206  cdlemk50  41208  cdlemk51  41209  cdlemk52  41210  cdlemk53a  41211  cdlemk39u  41224  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord11b  41478  dihord11c  41480  dihord2pre  41481  dihord2pre2  41482  dihord5apre  41518  dihmeetlem1N  41546  dihglblem2N  41550  dihglblem3N  41551  dihglbcpreN  41556  dihmeetlem3N  41561  dihjatc1  41567  dihjatc2N  41568  dihjatc3  41569  dihmeetlem15N  41577  infleinf  45612  mullimc  45858  mullimcf  45865  limsupre  45881  addlimc  45888  limclner  45891  sge0xaddlem2  46674  itscnhlc0xyqsol  49007  itsclquadb  49018  itsclquadeu  49019