Theorem simp11l 1281

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

Assertion

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

Proof of Theorem simp11l

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

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

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

This theorem is referenced by:  pceu  16785  maduf  22493  lshpsmreu  38491  exatleN  38787  2llnjaN  38949  2lplnja  39002  dalemkehl  39006  dath2  39120  pclfinN  39283  lhp2lt  39384  lhpexle3lem  39394  lhpmcvr5N  39410  lhpmcvr6N  39411  lhp2at0  39415  lhp2atnle  39416  lhp2atne  39417  lhp2at0nle  39418  lhp2at0ne  39419  4atexlemk  39430  4atexlemex6  39457  4atexlem7  39458  cdlemd2  39582  cdlemd4  39584  cdlemd7  39587  cdleme0ex2N  39607  cdleme7aa  39625  cdleme7c  39628  cdleme7d  39629  cdleme7e  39630  cdleme7ga  39631  cdleme7  39632  cdleme11c  39644  cdleme11dN  39645  cdleme11e  39646  cdleme11  39653  cdleme14  39656  cdleme15a  39657  cdleme15b  39658  cdleme15c  39659  cdleme15d  39660  cdleme15  39661  cdleme16b  39662  cdleme16c  39663  cdleme16d  39664  cdleme16e  39665  cdleme16f  39666  cdleme18d  39678  cdleme19b  39687  cdleme19d  39689  cdleme19e  39690  cdleme20d  39695  cdleme20e  39696  cdleme20f  39697  cdleme20g  39698  cdleme20h  39699  cdleme20j  39701  cdleme20k  39702  cdleme20l1  39703  cdleme20l2  39704  cdleme20l  39705  cdleme20m  39706  cdleme21c  39710  cdleme21ct  39712  cdleme21d  39713  cdleme21e  39714  cdleme22cN  39725  cdleme22f  39729  cdleme22f2  39730  cdleme22g  39731  cdleme23a  39732  cdleme23b  39733  cdleme23c  39734  cdleme25a  39736  cdleme25c  39738  cdleme25dN  39739  cdleme26ee  39743  cdleme26eALTN  39744  cdleme27a  39750  cdleme27N  39752  cdleme28a  39753  cdleme28b  39754  cdleme29ex  39757  cdlemefrs29bpre0  39779  cdlemefrs29cpre1  39781  cdlemefr29exN  39785  cdleme32fva  39820  cdleme32b  39825  cdleme32c  39826  cdleme32e  39828  cdleme35a  39831  cdleme35fnpq  39832  cdleme35b  39833  cdleme35c  39834  cdleme35d  39835  cdleme35e  39836  cdleme35f  39837  cdleme36a  39843  cdleme37m  39845  cdleme39a  39848  cdleme42e  39862  cdleme42h  39865  cdleme42i  39866  cdleme42k  39867  cdleme43bN  39873  cdleme43dN  39875  cdleme17d2  39878  cdleme48bw  39885  cdlemeg46c  39896  cdlemeg46nlpq  39900  cdlemeg46ngfr  39901  cdlemeg46frv  39908  cdlemeg46vrg  39910  cdlemeg46rgv  39911  cdlemeg46req  39912  cdlemeg46gfv  39913  cdlemf1  39944  trlord  39952  cdlemb3  39989  cdlemg7fvbwN  39990  cdlemg10a  40023  cdlemg10  40024  cdlemg12e  40030  cdlemg12f  40031  cdlemg12g  40032  cdlemg12  40033  cdlemg13a  40034  cdlemg13  40035  cdlemg17b  40045  cdlemg17g  40050  cdlemg17h  40051  cdlemg17pq  40055  cdlemg17  40060  cdlemg19a  40066  cdlemg19  40067  cdlemg21  40069  cdlemg27a  40075  cdlemg27b  40079  cdlemg31c  40082  cdlemg33b0  40084  cdlemg33c0  40085  cdlemg33a  40089  cdlemg33c  40091  cdlemg33e  40093  cdlemg35  40096  trlcone  40111  tendococl  40155  cdlemh1  40198  cdlemh2  40199  cdlemh  40200  cdlemi  40203  cdlemk5  40219  cdlemk6  40220  cdlemki  40224  cdlemksv2  40230  cdlemk7  40231  cdlemk11  40232  cdlemk12  40233  cdlemkole  40236  cdlemk14  40237  cdlemk15  40238  cdlemk17  40241  cdlemk1u  40242  cdlemk5u  40244  cdlemk6u  40245  cdlemkj  40246  cdlemkuv2  40250  cdlemk7u  40253  cdlemk11u  40254  cdlemk12u  40255  cdlemk26-3  40289  cdlemk37  40297  cdlemk11t  40329  cdlemk47  40332  cdlemk48  40333  cdlemk50  40335  cdlemk51  40336  cdlemk52  40337  cdlemk53a  40338  cdlemk39u  40351  dihord1  40601  dihord2a  40602  dihord2b  40603  dihord11b  40605  dihord11c  40607  dihord2pre  40608  dihord2pre2  40609  dihord5apre  40645  dihmeetlem1N  40673  dihglblem2N  40677  dihglblem3N  40678  dihglbcpreN  40683  dihmeetlem3N  40688  dihjatc1  40694  dihjatc2N  40695  dihjatc3  40696  dihmeetlem15N  40704  infleinf  44636  mullimc  44886  mullimcf  44893  limsupre  44911  addlimc  44918  limclner  44921  sge0xaddlem2  45704  itscnhlc0xyqsol  47708  itsclquadb  47719  itsclquadeu  47720