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  16817  maduf  22528  lshpsmreu  39102  exatleN  39398  2llnjaN  39560  2lplnja  39613  dalemkehl  39617  dath2  39731  pclfinN  39894  lhp2lt  39995  lhpexle3lem  40005  lhpmcvr5N  40021  lhpmcvr6N  40022  lhp2at0  40026  lhp2atnle  40027  lhp2atne  40028  lhp2at0nle  40029  lhp2at0ne  40030  4atexlemk  40041  4atexlemex6  40068  4atexlem7  40069  cdlemd2  40193  cdlemd4  40195  cdlemd7  40198  cdleme0ex2N  40218  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme11c  40255  cdleme11dN  40256  cdleme11e  40257  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme15b  40269  cdleme15c  40270  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme18d  40289  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20d  40306  cdleme20e  40307  cdleme20f  40308  cdleme20g  40309  cdleme20h  40310  cdleme20j  40312  cdleme20k  40313  cdleme20l1  40314  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21c  40321  cdleme21ct  40323  cdleme21d  40324  cdleme21e  40325  cdleme22cN  40336  cdleme22f  40340  cdleme22f2  40341  cdleme22g  40342  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme25a  40347  cdleme25c  40349  cdleme25dN  40350  cdleme26ee  40354  cdleme26eALTN  40355  cdleme27a  40361  cdleme27N  40363  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdlemefr29exN  40396  cdleme32fva  40431  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme36a  40454  cdleme37m  40456  cdleme39a  40459  cdleme42e  40473  cdleme42h  40476  cdleme42i  40477  cdleme42k  40478  cdleme43bN  40484  cdleme43dN  40486  cdleme17d2  40489  cdleme48bw  40496  cdlemeg46c  40507  cdlemeg46nlpq  40511  cdlemeg46ngfr  40512  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfv  40524  cdlemf1  40555  trlord  40563  cdlemb3  40600  cdlemg7fvbwN  40601  cdlemg10a  40634  cdlemg10  40635  cdlemg12e  40641  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg13  40646  cdlemg17b  40656  cdlemg17g  40661  cdlemg17h  40662  cdlemg17pq  40666  cdlemg17  40671  cdlemg19a  40677  cdlemg19  40678  cdlemg21  40680  cdlemg27a  40686  cdlemg27b  40690  cdlemg31c  40693  cdlemg33b0  40695  cdlemg33c0  40696  cdlemg33a  40700  cdlemg33c  40702  cdlemg33e  40704  cdlemg35  40707  trlcone  40722  tendococl  40766  cdlemh1  40809  cdlemh2  40810  cdlemh  40811  cdlemi  40814  cdlemk5  40830  cdlemk6  40831  cdlemki  40835  cdlemksv2  40841  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk17  40852  cdlemk1u  40853  cdlemk5u  40855  cdlemk6u  40856  cdlemkj  40857  cdlemkuv2  40861  cdlemk7u  40864  cdlemk11u  40865  cdlemk12u  40866  cdlemk26-3  40900  cdlemk37  40908  cdlemk11t  40940  cdlemk47  40943  cdlemk48  40944  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemk53a  40949  cdlemk39u  40962  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihord2pre2  41220  dihord5apre  41256  dihmeetlem1N  41284  dihglblem2N  41288  dihglblem3N  41289  dihglbcpreN  41294  dihmeetlem3N  41299  dihjatc1  41305  dihjatc2N  41306  dihjatc3  41307  dihmeetlem15N  41315  infleinf  45368  mullimc  45614  mullimcf  45621  limsupre  45639  addlimc  45646  limclner  45649  sge0xaddlem2  46432  itscnhlc0xyqsol  48754  itsclquadb  48765  itsclquadeu  48766