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  16864  maduf  22577  lshpsmreu  39073  exatleN  39369  2llnjaN  39531  2lplnja  39584  dalemkehl  39588  dath2  39702  pclfinN  39865  lhp2lt  39966  lhpexle3lem  39976  lhpmcvr5N  39992  lhpmcvr6N  39993  lhp2at0  39997  lhp2atnle  39998  lhp2atne  39999  lhp2at0nle  40000  lhp2at0ne  40001  4atexlemk  40012  4atexlemex6  40039  4atexlem7  40040  cdlemd2  40164  cdlemd4  40166  cdlemd7  40169  cdleme0ex2N  40189  cdleme7aa  40207  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme11c  40226  cdleme11dN  40227  cdleme11e  40228  cdleme11  40235  cdleme14  40238  cdleme15a  40239  cdleme15b  40240  cdleme15c  40241  cdleme15d  40242  cdleme15  40243  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme18d  40260  cdleme19b  40269  cdleme19d  40271  cdleme19e  40272  cdleme20d  40277  cdleme20e  40278  cdleme20f  40279  cdleme20g  40280  cdleme20h  40281  cdleme20j  40283  cdleme20k  40284  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21c  40292  cdleme21ct  40294  cdleme21d  40295  cdleme21e  40296  cdleme22cN  40307  cdleme22f  40311  cdleme22f2  40312  cdleme22g  40313  cdleme23a  40314  cdleme23b  40315  cdleme23c  40316  cdleme25a  40318  cdleme25c  40320  cdleme25dN  40321  cdleme26ee  40325  cdleme26eALTN  40326  cdleme27a  40332  cdleme27N  40334  cdleme28a  40335  cdleme28b  40336  cdleme29ex  40339  cdlemefrs29bpre0  40361  cdlemefrs29cpre1  40363  cdlemefr29exN  40367  cdleme32fva  40402  cdleme32b  40407  cdleme32c  40408  cdleme32e  40410  cdleme35a  40413  cdleme35fnpq  40414  cdleme35b  40415  cdleme35c  40416  cdleme35d  40417  cdleme35e  40418  cdleme35f  40419  cdleme36a  40425  cdleme37m  40427  cdleme39a  40430  cdleme42e  40444  cdleme42h  40447  cdleme42i  40448  cdleme42k  40449  cdleme43bN  40455  cdleme43dN  40457  cdleme17d2  40460  cdleme48bw  40467  cdlemeg46c  40478  cdlemeg46nlpq  40482  cdlemeg46ngfr  40483  cdlemeg46frv  40490  cdlemeg46vrg  40492  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemeg46gfv  40495  cdlemf1  40526  trlord  40534  cdlemb3  40571  cdlemg7fvbwN  40572  cdlemg10a  40605  cdlemg10  40606  cdlemg12e  40612  cdlemg12f  40613  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg13  40617  cdlemg17b  40627  cdlemg17g  40632  cdlemg17h  40633  cdlemg17pq  40637  cdlemg17  40642  cdlemg19a  40648  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg27b  40661  cdlemg31c  40664  cdlemg33b0  40666  cdlemg33c0  40667  cdlemg33a  40671  cdlemg33c  40673  cdlemg33e  40675  cdlemg35  40678  trlcone  40693  tendococl  40737  cdlemh1  40780  cdlemh2  40781  cdlemh  40782  cdlemi  40785  cdlemk5  40801  cdlemk6  40802  cdlemki  40806  cdlemksv2  40812  cdlemk7  40813  cdlemk11  40814  cdlemk12  40815  cdlemkole  40818  cdlemk14  40819  cdlemk15  40820  cdlemk17  40823  cdlemk1u  40824  cdlemk5u  40826  cdlemk6u  40827  cdlemkj  40828  cdlemkuv2  40832  cdlemk7u  40835  cdlemk11u  40836  cdlemk12u  40837  cdlemk26-3  40871  cdlemk37  40879  cdlemk11t  40911  cdlemk47  40914  cdlemk48  40915  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk39u  40933  dihord1  41183  dihord2a  41184  dihord2b  41185  dihord11b  41187  dihord11c  41189  dihord2pre  41190  dihord2pre2  41191  dihord5apre  41227  dihmeetlem1N  41255  dihglblem2N  41259  dihglblem3N  41260  dihglbcpreN  41265  dihmeetlem3N  41270  dihjatc1  41276  dihjatc2N  41277  dihjatc3  41278  dihmeetlem15N  41286  infleinf  45347  mullimc  45593  mullimcf  45600  limsupre  45618  addlimc  45625  limclner  45628  sge0xaddlem2  46411  itscnhlc0xyqsol  48693  itsclquadb  48704  itsclquadeu  48705