Theorem simp11l 1303

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

Assertion

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

Proof of Theorem simp11l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  16944  maduf  22869  lshpsmreu  39990  exatleN  40285  2llnjaN  40447  2lplnja  40500  dalemkehl  40504  dath2  40618  pclfinN  40781  lhp2lt  40882  lhpexle3lem  40892  lhpmcvr5N  40908  lhpmcvr6N  40909  lhp2at0  40913  lhp2atnle  40914  lhp2atne  40915  lhp2at0nle  40916  lhp2at0ne  40917  4atexlemk  40928  4atexlemex6  40955  4atexlem7  40956  cdlemd2  41080  cdlemd4  41082  cdlemd7  41085  cdleme0ex2N  41105  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11c  41142  cdleme11dN  41143  cdleme11e  41144  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15b  41156  cdleme15c  41157  cdleme15d  41158  cdleme15  41159  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme16f  41164  cdleme18d  41176  cdleme19b  41185  cdleme19d  41187  cdleme19e  41188  cdleme20d  41193  cdleme20e  41194  cdleme20f  41195  cdleme20g  41196  cdleme20h  41197  cdleme20j  41199  cdleme20k  41200  cdleme20l1  41201  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21c  41208  cdleme21ct  41210  cdleme21d  41211  cdleme21e  41212  cdleme22cN  41223  cdleme22f  41227  cdleme22f2  41228  cdleme22g  41229  cdleme23a  41230  cdleme23b  41231  cdleme23c  41232  cdleme25a  41234  cdleme25c  41236  cdleme25dN  41237  cdleme26ee  41241  cdleme26eALTN  41242  cdleme27a  41248  cdleme27N  41250  cdleme28a  41251  cdleme28b  41252  cdleme29ex  41255  cdlemefrs29bpre0  41277  cdlemefrs29cpre1  41279  cdlemefr29exN  41283  cdleme32fva  41318  cdleme32b  41323  cdleme32c  41324  cdleme32e  41326  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35e  41334  cdleme35f  41335  cdleme36a  41341  cdleme37m  41343  cdleme39a  41346  cdleme42e  41360  cdleme42h  41363  cdleme42i  41364  cdleme42k  41365  cdleme43bN  41371  cdleme43dN  41373  cdleme17d2  41376  cdleme48bw  41383  cdlemeg46c  41394  cdlemeg46nlpq  41398  cdlemeg46ngfr  41399  cdlemeg46frv  41406  cdlemeg46vrg  41408  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemeg46gfv  41411  cdlemf1  41442  trlord  41450  cdlemb3  41487  cdlemg7fvbwN  41488  cdlemg10a  41521  cdlemg10  41522  cdlemg12e  41528  cdlemg12f  41529  cdlemg12g  41530  cdlemg12  41531  cdlemg13a  41532  cdlemg13  41533  cdlemg17b  41543  cdlemg17g  41548  cdlemg17h  41549  cdlemg17pq  41553  cdlemg17  41558  cdlemg19a  41564  cdlemg19  41565  cdlemg21  41567  cdlemg27a  41573  cdlemg27b  41577  cdlemg31c  41580  cdlemg33b0  41582  cdlemg33c0  41583  cdlemg33a  41587  cdlemg33c  41589  cdlemg33e  41591  cdlemg35  41594  trlcone  41609  tendococl  41653  cdlemh1  41696  cdlemh2  41697  cdlemh  41698  cdlemi  41701  cdlemk5  41717  cdlemk6  41718  cdlemki  41722  cdlemksv2  41728  cdlemk7  41729  cdlemk11  41730  cdlemk12  41731  cdlemkole  41734  cdlemk14  41735  cdlemk15  41736  cdlemk17  41739  cdlemk1u  41740  cdlemk5u  41742  cdlemk6u  41743  cdlemkj  41744  cdlemkuv2  41748  cdlemk7u  41751  cdlemk11u  41752  cdlemk12u  41753  cdlemk26-3  41787  cdlemk37  41795  cdlemk11t  41827  cdlemk47  41830  cdlemk48  41831  cdlemk50  41833  cdlemk51  41834  cdlemk52  41835  cdlemk53a  41836  cdlemk39u  41849  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord11b  42103  dihord11c  42105  dihord2pre  42106  dihord2pre2  42107  dihord5apre  42143  dihmeetlem1N  42171  dihglblem2N  42175  dihglblem3N  42176  dihglbcpreN  42181  dihmeetlem3N  42186  dihjatc1  42192  dihjatc2N  42193  dihjatc3  42194  dihmeetlem15N  42202  infleinf  46209  mullimc  46454  mullimcf  46461  limsupre  46477  addlimc  46484  limclner  46487  sge0xaddlem2  47270  itscnhlc0xyqsol  49703  itsclquadb  49714  itsclquadeu  49715