Theorem simp11l 1280

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pceu  16177  maduf  21244  lshpsmreu  36239  exatleN  36534  2llnjaN  36696  2lplnja  36749  dalemkehl  36753  dath2  36867  pclfinN  37030  lhp2lt  37131  lhpexle3lem  37141  lhpmcvr5N  37157  lhpmcvr6N  37158  lhp2at0  37162  lhp2atnle  37163  lhp2atne  37164  lhp2at0nle  37165  lhp2at0ne  37166  4atexlemk  37177  4atexlemex6  37204  4atexlem7  37205  cdlemd2  37329  cdlemd4  37331  cdlemd7  37334  cdleme0ex2N  37354  cdleme7aa  37372  cdleme7c  37375  cdleme7d  37376  cdleme7e  37377  cdleme7ga  37378  cdleme7  37379  cdleme11c  37391  cdleme11dN  37392  cdleme11e  37393  cdleme11  37400  cdleme14  37403  cdleme15a  37404  cdleme15b  37405  cdleme15c  37406  cdleme15d  37407  cdleme15  37408  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme18d  37425  cdleme19b  37434  cdleme19d  37436  cdleme19e  37437  cdleme20d  37442  cdleme20e  37443  cdleme20f  37444  cdleme20g  37445  cdleme20h  37446  cdleme20j  37448  cdleme20k  37449  cdleme20l1  37450  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21c  37457  cdleme21ct  37459  cdleme21d  37460  cdleme21e  37461  cdleme22cN  37472  cdleme22f  37476  cdleme22f2  37477  cdleme22g  37478  cdleme23a  37479  cdleme23b  37480  cdleme23c  37481  cdleme25a  37483  cdleme25c  37485  cdleme25dN  37486  cdleme26ee  37490  cdleme26eALTN  37491  cdleme27a  37497  cdleme27N  37499  cdleme28a  37500  cdleme28b  37501  cdleme29ex  37504  cdlemefrs29bpre0  37526  cdlemefrs29cpre1  37528  cdlemefr29exN  37532  cdleme32fva  37567  cdleme32b  37572  cdleme32c  37573  cdleme32e  37575  cdleme35a  37578  cdleme35fnpq  37579  cdleme35b  37580  cdleme35c  37581  cdleme35d  37582  cdleme35e  37583  cdleme35f  37584  cdleme36a  37590  cdleme37m  37592  cdleme39a  37595  cdleme42e  37609  cdleme42h  37612  cdleme42i  37613  cdleme42k  37614  cdleme43bN  37620  cdleme43dN  37622  cdleme17d2  37625  cdleme48bw  37632  cdlemeg46c  37643  cdlemeg46nlpq  37647  cdlemeg46ngfr  37648  cdlemeg46frv  37655  cdlemeg46vrg  37657  cdlemeg46rgv  37658  cdlemeg46req  37659  cdlemeg46gfv  37660  cdlemf1  37691  trlord  37699  cdlemb3  37736  cdlemg7fvbwN  37737  cdlemg10a  37770  cdlemg10  37771  cdlemg12e  37777  cdlemg12f  37778  cdlemg12g  37779  cdlemg12  37780  cdlemg13a  37781  cdlemg13  37782  cdlemg17b  37792  cdlemg17g  37797  cdlemg17h  37798  cdlemg17pq  37802  cdlemg17  37807  cdlemg19a  37813  cdlemg19  37814  cdlemg21  37816  cdlemg27a  37822  cdlemg27b  37826  cdlemg31c  37829  cdlemg33b0  37831  cdlemg33c0  37832  cdlemg33a  37836  cdlemg33c  37838  cdlemg33e  37840  cdlemg35  37843  trlcone  37858  tendococl  37902  cdlemh1  37945  cdlemh2  37946  cdlemh  37947  cdlemi  37950  cdlemk5  37966  cdlemk6  37967  cdlemki  37971  cdlemksv2  37977  cdlemk7  37978  cdlemk11  37979  cdlemk12  37980  cdlemkole  37983  cdlemk14  37984  cdlemk15  37985  cdlemk17  37988  cdlemk1u  37989  cdlemk5u  37991  cdlemk6u  37992  cdlemkj  37993  cdlemkuv2  37997  cdlemk7u  38000  cdlemk11u  38001  cdlemk12u  38002  cdlemk26-3  38036  cdlemk37  38044  cdlemk11t  38076  cdlemk47  38079  cdlemk48  38080  cdlemk50  38082  cdlemk51  38083  cdlemk52  38084  cdlemk53a  38085  cdlemk39u  38098  dihord1  38348  dihord2a  38349  dihord2b  38350  dihord11b  38352  dihord11c  38354  dihord2pre  38355  dihord2pre2  38356  dihord5apre  38392  dihmeetlem1N  38420  dihglblem2N  38424  dihglblem3N  38425  dihglbcpreN  38430  dihmeetlem3N  38435  dihjatc1  38441  dihjatc2N  38442  dihjatc3  38443  dihmeetlem15N  38451  infleinf  41633  mullimc  41890  mullimcf  41897  limsupre  41915  addlimc  41922  limclner  41925  sge0xaddlem2  42710  itscnhlc0xyqsol  44746  itsclquadb  44757  itsclquadeu  44758