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 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  16866  maduf  22595  lshpsmreu  39069  exatleN  39365  2llnjaN  39527  2lplnja  39580  dalemkehl  39584  dath2  39698  pclfinN  39861  lhp2lt  39962  lhpexle3lem  39972  lhpmcvr5N  39988  lhpmcvr6N  39989  lhp2at0  39993  lhp2atnle  39994  lhp2atne  39995  lhp2at0nle  39996  lhp2at0ne  39997  4atexlemk  40008  4atexlemex6  40035  4atexlem7  40036  cdlemd2  40160  cdlemd4  40162  cdlemd7  40165  cdleme0ex2N  40185  cdleme7aa  40203  cdleme7c  40206  cdleme7d  40207  cdleme7e  40208  cdleme7ga  40209  cdleme7  40210  cdleme11c  40222  cdleme11dN  40223  cdleme11e  40224  cdleme11  40231  cdleme14  40234  cdleme15a  40235  cdleme15b  40236  cdleme15c  40237  cdleme15d  40238  cdleme15  40239  cdleme16b  40240  cdleme16c  40241  cdleme16d  40242  cdleme16e  40243  cdleme16f  40244  cdleme18d  40256  cdleme19b  40265  cdleme19d  40267  cdleme19e  40268  cdleme20d  40273  cdleme20e  40274  cdleme20f  40275  cdleme20g  40276  cdleme20h  40277  cdleme20j  40279  cdleme20k  40280  cdleme20l1  40281  cdleme20l2  40282  cdleme20l  40283  cdleme20m  40284  cdleme21c  40288  cdleme21ct  40290  cdleme21d  40291  cdleme21e  40292  cdleme22cN  40303  cdleme22f  40307  cdleme22f2  40308  cdleme22g  40309  cdleme23a  40310  cdleme23b  40311  cdleme23c  40312  cdleme25a  40314  cdleme25c  40316  cdleme25dN  40317  cdleme26ee  40321  cdleme26eALTN  40322  cdleme27a  40328  cdleme27N  40330  cdleme28a  40331  cdleme28b  40332  cdleme29ex  40335  cdlemefrs29bpre0  40357  cdlemefrs29cpre1  40359  cdlemefr29exN  40363  cdleme32fva  40398  cdleme32b  40403  cdleme32c  40404  cdleme32e  40406  cdleme35a  40409  cdleme35fnpq  40410  cdleme35b  40411  cdleme35c  40412  cdleme35d  40413  cdleme35e  40414  cdleme35f  40415  cdleme36a  40421  cdleme37m  40423  cdleme39a  40426  cdleme42e  40440  cdleme42h  40443  cdleme42i  40444  cdleme42k  40445  cdleme43bN  40451  cdleme43dN  40453  cdleme17d2  40456  cdleme48bw  40463  cdlemeg46c  40474  cdlemeg46nlpq  40478  cdlemeg46ngfr  40479  cdlemeg46frv  40486  cdlemeg46vrg  40488  cdlemeg46rgv  40489  cdlemeg46req  40490  cdlemeg46gfv  40491  cdlemf1  40522  trlord  40530  cdlemb3  40567  cdlemg7fvbwN  40568  cdlemg10a  40601  cdlemg10  40602  cdlemg12e  40608  cdlemg12f  40609  cdlemg12g  40610  cdlemg12  40611  cdlemg13a  40612  cdlemg13  40613  cdlemg17b  40623  cdlemg17g  40628  cdlemg17h  40629  cdlemg17pq  40633  cdlemg17  40638  cdlemg19a  40644  cdlemg19  40645  cdlemg21  40647  cdlemg27a  40653  cdlemg27b  40657  cdlemg31c  40660  cdlemg33b0  40662  cdlemg33c0  40663  cdlemg33a  40667  cdlemg33c  40669  cdlemg33e  40671  cdlemg35  40674  trlcone  40689  tendococl  40733  cdlemh1  40776  cdlemh2  40777  cdlemh  40778  cdlemi  40781  cdlemk5  40797  cdlemk6  40798  cdlemki  40802  cdlemksv2  40808  cdlemk7  40809  cdlemk11  40810  cdlemk12  40811  cdlemkole  40814  cdlemk14  40815  cdlemk15  40816  cdlemk17  40819  cdlemk1u  40820  cdlemk5u  40822  cdlemk6u  40823  cdlemkj  40824  cdlemkuv2  40828  cdlemk7u  40831  cdlemk11u  40832  cdlemk12u  40833  cdlemk26-3  40867  cdlemk37  40875  cdlemk11t  40907  cdlemk47  40910  cdlemk48  40911  cdlemk50  40913  cdlemk51  40914  cdlemk52  40915  cdlemk53a  40916  cdlemk39u  40929  dihord1  41179  dihord2a  41180  dihord2b  41181  dihord11b  41183  dihord11c  41185  dihord2pre  41186  dihord2pre2  41187  dihord5apre  41223  dihmeetlem1N  41251  dihglblem2N  41255  dihglblem3N  41256  dihglbcpreN  41261  dihmeetlem3N  41266  dihjatc1  41272  dihjatc2N  41273  dihjatc3  41274  dihmeetlem15N  41282  infleinf  45340  mullimc  45588  mullimcf  45595  limsupre  45613  addlimc  45620  limclner  45623  sge0xaddlem2  46406  itscnhlc0xyqsol  48644  itsclquadb  48655  itsclquadeu  48656