Theorem simp11l 1291

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  pceu  16815  maduf  22631  lshpsmreu  39608  exatleN  39903  2llnjaN  40065  2lplnja  40118  dalemkehl  40122  dath2  40236  pclfinN  40399  lhp2lt  40500  lhpexle3lem  40510  lhpmcvr5N  40526  lhpmcvr6N  40527  lhp2at0  40531  lhp2atnle  40532  lhp2atne  40533  lhp2at0nle  40534  lhp2at0ne  40535  4atexlemk  40546  4atexlemex6  40573  4atexlem7  40574  cdlemd2  40698  cdlemd4  40700  cdlemd7  40703  cdleme0ex2N  40723  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11c  40760  cdleme11dN  40761  cdleme11e  40762  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15b  40774  cdleme15c  40775  cdleme15d  40776  cdleme15  40777  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme16f  40782  cdleme18d  40794  cdleme19b  40803  cdleme19d  40805  cdleme19e  40806  cdleme20d  40811  cdleme20e  40812  cdleme20f  40813  cdleme20g  40814  cdleme20h  40815  cdleme20j  40817  cdleme20k  40818  cdleme20l1  40819  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21c  40826  cdleme21ct  40828  cdleme21d  40829  cdleme21e  40830  cdleme22cN  40841  cdleme22f  40845  cdleme22f2  40846  cdleme22g  40847  cdleme23a  40848  cdleme23b  40849  cdleme23c  40850  cdleme25a  40852  cdleme25c  40854  cdleme25dN  40855  cdleme26ee  40859  cdleme26eALTN  40860  cdleme27a  40866  cdleme27N  40868  cdleme28a  40869  cdleme28b  40870  cdleme29ex  40873  cdlemefrs29bpre0  40895  cdlemefrs29cpre1  40897  cdlemefr29exN  40901  cdleme32fva  40936  cdleme32b  40941  cdleme32c  40942  cdleme32e  40944  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35e  40952  cdleme35f  40953  cdleme36a  40959  cdleme37m  40961  cdleme39a  40964  cdleme42e  40978  cdleme42h  40981  cdleme42i  40982  cdleme42k  40983  cdleme43bN  40989  cdleme43dN  40991  cdleme17d2  40994  cdleme48bw  41001  cdlemeg46c  41012  cdlemeg46nlpq  41016  cdlemeg46ngfr  41017  cdlemeg46frv  41024  cdlemeg46vrg  41026  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemeg46gfv  41029  cdlemf1  41060  trlord  41068  cdlemb3  41105  cdlemg7fvbwN  41106  cdlemg10a  41139  cdlemg10  41140  cdlemg12e  41146  cdlemg12f  41147  cdlemg12g  41148  cdlemg12  41149  cdlemg13a  41150  cdlemg13  41151  cdlemg17b  41161  cdlemg17g  41166  cdlemg17h  41167  cdlemg17pq  41171  cdlemg17  41176  cdlemg19a  41182  cdlemg19  41183  cdlemg21  41185  cdlemg27a  41191  cdlemg27b  41195  cdlemg31c  41198  cdlemg33b0  41200  cdlemg33c0  41201  cdlemg33a  41205  cdlemg33c  41207  cdlemg33e  41209  cdlemg35  41212  trlcone  41227  tendococl  41271  cdlemh1  41314  cdlemh2  41315  cdlemh  41316  cdlemi  41319  cdlemk5  41335  cdlemk6  41336  cdlemki  41340  cdlemksv2  41346  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemkole  41352  cdlemk14  41353  cdlemk15  41354  cdlemk17  41357  cdlemk1u  41358  cdlemk5u  41360  cdlemk6u  41361  cdlemkj  41362  cdlemkuv2  41366  cdlemk7u  41369  cdlemk11u  41370  cdlemk12u  41371  cdlemk26-3  41405  cdlemk37  41413  cdlemk11t  41445  cdlemk47  41448  cdlemk48  41449  cdlemk50  41451  cdlemk51  41452  cdlemk52  41453  cdlemk53a  41454  cdlemk39u  41467  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord11b  41721  dihord11c  41723  dihord2pre  41724  dihord2pre2  41725  dihord5apre  41761  dihmeetlem1N  41789  dihglblem2N  41793  dihglblem3N  41794  dihglbcpreN  41799  dihmeetlem3N  41804  dihjatc1  41810  dihjatc2N  41811  dihjatc3  41812  dihmeetlem15N  41820  infleinf  45823  mullimc  46068  mullimcf  46075  limsupre  46091  addlimc  46098  limclner  46101  sge0xaddlem2  46884  itscnhlc0xyqsol  49263  itsclquadb  49274  itsclquadeu  49275