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  16776  maduf  22544  lshpsmreu  39087  exatleN  39383  2llnjaN  39545  2lplnja  39598  dalemkehl  39602  dath2  39716  pclfinN  39879  lhp2lt  39980  lhpexle3lem  39990  lhpmcvr5N  40006  lhpmcvr6N  40007  lhp2at0  40011  lhp2atnle  40012  lhp2atne  40013  lhp2at0nle  40014  lhp2at0ne  40015  4atexlemk  40026  4atexlemex6  40053  4atexlem7  40054  cdlemd2  40178  cdlemd4  40180  cdlemd7  40183  cdleme0ex2N  40203  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11c  40240  cdleme11dN  40241  cdleme11e  40242  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15b  40254  cdleme15c  40255  cdleme15d  40256  cdleme15  40257  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme18d  40274  cdleme19b  40283  cdleme19d  40285  cdleme19e  40286  cdleme20d  40291  cdleme20e  40292  cdleme20f  40293  cdleme20g  40294  cdleme20h  40295  cdleme20j  40297  cdleme20k  40298  cdleme20l1  40299  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21c  40306  cdleme21ct  40308  cdleme21d  40309  cdleme21e  40310  cdleme22cN  40321  cdleme22f  40325  cdleme22f2  40326  cdleme22g  40327  cdleme23a  40328  cdleme23b  40329  cdleme23c  40330  cdleme25a  40332  cdleme25c  40334  cdleme25dN  40335  cdleme26ee  40339  cdleme26eALTN  40340  cdleme27a  40346  cdleme27N  40348  cdleme28a  40349  cdleme28b  40350  cdleme29ex  40353  cdlemefrs29bpre0  40375  cdlemefrs29cpre1  40377  cdlemefr29exN  40381  cdleme32fva  40416  cdleme32b  40421  cdleme32c  40422  cdleme32e  40424  cdleme35a  40427  cdleme35fnpq  40428  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35e  40432  cdleme35f  40433  cdleme36a  40439  cdleme37m  40441  cdleme39a  40444  cdleme42e  40458  cdleme42h  40461  cdleme42i  40462  cdleme42k  40463  cdleme43bN  40469  cdleme43dN  40471  cdleme17d2  40474  cdleme48bw  40481  cdlemeg46c  40492  cdlemeg46nlpq  40496  cdlemeg46ngfr  40497  cdlemeg46frv  40504  cdlemeg46vrg  40506  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemeg46gfv  40509  cdlemf1  40540  trlord  40548  cdlemb3  40585  cdlemg7fvbwN  40586  cdlemg10a  40619  cdlemg10  40620  cdlemg12e  40626  cdlemg12f  40627  cdlemg12g  40628  cdlemg12  40629  cdlemg13a  40630  cdlemg13  40631  cdlemg17b  40641  cdlemg17g  40646  cdlemg17h  40647  cdlemg17pq  40651  cdlemg17  40656  cdlemg19a  40662  cdlemg19  40663  cdlemg21  40665  cdlemg27a  40671  cdlemg27b  40675  cdlemg31c  40678  cdlemg33b0  40680  cdlemg33c0  40681  cdlemg33a  40685  cdlemg33c  40687  cdlemg33e  40689  cdlemg35  40692  trlcone  40707  tendococl  40751  cdlemh1  40794  cdlemh2  40795  cdlemh  40796  cdlemi  40799  cdlemk5  40815  cdlemk6  40816  cdlemki  40820  cdlemksv2  40826  cdlemk7  40827  cdlemk11  40828  cdlemk12  40829  cdlemkole  40832  cdlemk14  40833  cdlemk15  40834  cdlemk17  40837  cdlemk1u  40838  cdlemk5u  40840  cdlemk6u  40841  cdlemkj  40842  cdlemkuv2  40846  cdlemk7u  40849  cdlemk11u  40850  cdlemk12u  40851  cdlemk26-3  40885  cdlemk37  40893  cdlemk11t  40925  cdlemk47  40928  cdlemk48  40929  cdlemk50  40931  cdlemk51  40932  cdlemk52  40933  cdlemk53a  40934  cdlemk39u  40947  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord11b  41201  dihord11c  41203  dihord2pre  41204  dihord2pre2  41205  dihord5apre  41241  dihmeetlem1N  41269  dihglblem2N  41273  dihglblem3N  41274  dihglbcpreN  41279  dihmeetlem3N  41284  dihjatc1  41290  dihjatc2N  41291  dihjatc3  41292  dihmeetlem15N  41300  infleinf  45352  mullimc  45598  mullimcf  45605  limsupre  45623  addlimc  45630  limclner  45633  sge0xaddlem2  46416  itscnhlc0xyqsol  48751  itsclquadb  48762  itsclquadeu  48763