Theorem simp11l 1283

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pceu  16556  maduf  21799  lshpsmreu  37130  exatleN  37425  2llnjaN  37587  2lplnja  37640  dalemkehl  37644  dath2  37758  pclfinN  37921  lhp2lt  38022  lhpexle3lem  38032  lhpmcvr5N  38048  lhpmcvr6N  38049  lhp2at0  38053  lhp2atnle  38054  lhp2atne  38055  lhp2at0nle  38056  lhp2at0ne  38057  4atexlemk  38068  4atexlemex6  38095  4atexlem7  38096  cdlemd2  38220  cdlemd4  38222  cdlemd7  38225  cdleme0ex2N  38245  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme11c  38282  cdleme11dN  38283  cdleme11e  38284  cdleme11  38291  cdleme14  38294  cdleme15a  38295  cdleme15b  38296  cdleme15c  38297  cdleme15d  38298  cdleme15  38299  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme18d  38316  cdleme19b  38325  cdleme19d  38327  cdleme19e  38328  cdleme20d  38333  cdleme20e  38334  cdleme20f  38335  cdleme20g  38336  cdleme20h  38337  cdleme20j  38339  cdleme20k  38340  cdleme20l1  38341  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21c  38348  cdleme21ct  38350  cdleme21d  38351  cdleme21e  38352  cdleme22cN  38363  cdleme22f  38367  cdleme22f2  38368  cdleme22g  38369  cdleme23a  38370  cdleme23b  38371  cdleme23c  38372  cdleme25a  38374  cdleme25c  38376  cdleme25dN  38377  cdleme26ee  38381  cdleme26eALTN  38382  cdleme27a  38388  cdleme27N  38390  cdleme28a  38391  cdleme28b  38392  cdleme29ex  38395  cdlemefrs29bpre0  38417  cdlemefrs29cpre1  38419  cdlemefr29exN  38423  cdleme32fva  38458  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35e  38474  cdleme35f  38475  cdleme36a  38481  cdleme37m  38483  cdleme39a  38486  cdleme42e  38500  cdleme42h  38503  cdleme42i  38504  cdleme42k  38505  cdleme43bN  38511  cdleme43dN  38513  cdleme17d2  38516  cdleme48bw  38523  cdlemeg46c  38534  cdlemeg46nlpq  38538  cdlemeg46ngfr  38539  cdlemeg46frv  38546  cdlemeg46vrg  38548  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfv  38551  cdlemf1  38582  trlord  38590  cdlemb3  38627  cdlemg7fvbwN  38628  cdlemg10a  38661  cdlemg10  38662  cdlemg12e  38668  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg13  38673  cdlemg17b  38683  cdlemg17g  38688  cdlemg17h  38689  cdlemg17pq  38693  cdlemg17  38698  cdlemg19a  38704  cdlemg19  38705  cdlemg21  38707  cdlemg27a  38713  cdlemg27b  38717  cdlemg31c  38720  cdlemg33b0  38722  cdlemg33c0  38723  cdlemg33a  38727  cdlemg33c  38729  cdlemg33e  38731  cdlemg35  38734  trlcone  38749  tendococl  38793  cdlemh1  38836  cdlemh2  38837  cdlemh  38838  cdlemi  38841  cdlemk5  38857  cdlemk6  38858  cdlemki  38862  cdlemksv2  38868  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk17  38879  cdlemk1u  38880  cdlemk5u  38882  cdlemk6u  38883  cdlemkj  38884  cdlemkuv2  38888  cdlemk7u  38891  cdlemk11u  38892  cdlemk12u  38893  cdlemk26-3  38927  cdlemk37  38935  cdlemk11t  38967  cdlemk47  38970  cdlemk48  38971  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk53a  38976  cdlemk39u  38989  dihord1  39239  dihord2a  39240  dihord2b  39241  dihord11b  39243  dihord11c  39245  dihord2pre  39246  dihord2pre2  39247  dihord5apre  39283  dihmeetlem1N  39311  dihglblem2N  39315  dihglblem3N  39316  dihglbcpreN  39321  dihmeetlem3N  39326  dihjatc1  39332  dihjatc2N  39333  dihjatc3  39334  dihmeetlem15N  39342  infleinf  42918  mullimc  43164  mullimcf  43171  limsupre  43189  addlimc  43196  limclner  43199  sge0xaddlem2  43979  itscnhlc0xyqsol  46122  itsclquadb  46133  itsclquadeu  46134