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  16185  maduf  21252  lshpsmreu  36247  exatleN  36542  2llnjaN  36704  2lplnja  36757  dalemkehl  36761  dath2  36875  pclfinN  37038  lhp2lt  37139  lhpexle3lem  37149  lhpmcvr5N  37165  lhpmcvr6N  37166  lhp2at0  37170  lhp2atnle  37171  lhp2atne  37172  lhp2at0nle  37173  lhp2at0ne  37174  4atexlemk  37185  4atexlemex6  37212  4atexlem7  37213  cdlemd2  37337  cdlemd4  37339  cdlemd7  37342  cdleme0ex2N  37362  cdleme7aa  37380  cdleme7c  37383  cdleme7d  37384  cdleme7e  37385  cdleme7ga  37386  cdleme7  37387  cdleme11c  37399  cdleme11dN  37400  cdleme11e  37401  cdleme11  37408  cdleme14  37411  cdleme15a  37412  cdleme15b  37413  cdleme15c  37414  cdleme15d  37415  cdleme15  37416  cdleme16b  37417  cdleme16c  37418  cdleme16d  37419  cdleme16e  37420  cdleme16f  37421  cdleme18d  37433  cdleme19b  37442  cdleme19d  37444  cdleme19e  37445  cdleme20d  37450  cdleme20e  37451  cdleme20f  37452  cdleme20g  37453  cdleme20h  37454  cdleme20j  37456  cdleme20k  37457  cdleme20l1  37458  cdleme20l2  37459  cdleme20l  37460  cdleme20m  37461  cdleme21c  37465  cdleme21ct  37467  cdleme21d  37468  cdleme21e  37469  cdleme22cN  37480  cdleme22f  37484  cdleme22f2  37485  cdleme22g  37486  cdleme23a  37487  cdleme23b  37488  cdleme23c  37489  cdleme25a  37491  cdleme25c  37493  cdleme25dN  37494  cdleme26ee  37498  cdleme26eALTN  37499  cdleme27a  37505  cdleme27N  37507  cdleme28a  37508  cdleme28b  37509  cdleme29ex  37512  cdlemefrs29bpre0  37534  cdlemefrs29cpre1  37536  cdlemefr29exN  37540  cdleme32fva  37575  cdleme32b  37580  cdleme32c  37581  cdleme32e  37583  cdleme35a  37586  cdleme35fnpq  37587  cdleme35b  37588  cdleme35c  37589  cdleme35d  37590  cdleme35e  37591  cdleme35f  37592  cdleme36a  37598  cdleme37m  37600  cdleme39a  37603  cdleme42e  37617  cdleme42h  37620  cdleme42i  37621  cdleme42k  37622  cdleme43bN  37628  cdleme43dN  37630  cdleme17d2  37633  cdleme48bw  37640  cdlemeg46c  37651  cdlemeg46nlpq  37655  cdlemeg46ngfr  37656  cdlemeg46frv  37663  cdlemeg46vrg  37665  cdlemeg46rgv  37666  cdlemeg46req  37667  cdlemeg46gfv  37668  cdlemf1  37699  trlord  37707  cdlemb3  37744  cdlemg7fvbwN  37745  cdlemg10a  37778  cdlemg10  37779  cdlemg12e  37785  cdlemg12f  37786  cdlemg12g  37787  cdlemg12  37788  cdlemg13a  37789  cdlemg13  37790  cdlemg17b  37800  cdlemg17g  37805  cdlemg17h  37806  cdlemg17pq  37810  cdlemg17  37815  cdlemg19a  37821  cdlemg19  37822  cdlemg21  37824  cdlemg27a  37830  cdlemg27b  37834  cdlemg31c  37837  cdlemg33b0  37839  cdlemg33c0  37840  cdlemg33a  37844  cdlemg33c  37846  cdlemg33e  37848  cdlemg35  37851  trlcone  37866  tendococl  37910  cdlemh1  37953  cdlemh2  37954  cdlemh  37955  cdlemi  37958  cdlemk5  37974  cdlemk6  37975  cdlemki  37979  cdlemksv2  37985  cdlemk7  37986  cdlemk11  37987  cdlemk12  37988  cdlemkole  37991  cdlemk14  37992  cdlemk15  37993  cdlemk17  37996  cdlemk1u  37997  cdlemk5u  37999  cdlemk6u  38000  cdlemkj  38001  cdlemkuv2  38005  cdlemk7u  38008  cdlemk11u  38009  cdlemk12u  38010  cdlemk26-3  38044  cdlemk37  38052  cdlemk11t  38084  cdlemk47  38087  cdlemk48  38088  cdlemk50  38090  cdlemk51  38091  cdlemk52  38092  cdlemk53a  38093  cdlemk39u  38106  dihord1  38356  dihord2a  38357  dihord2b  38358  dihord11b  38360  dihord11c  38362  dihord2pre  38363  dihord2pre2  38364  dihord5apre  38400  dihmeetlem1N  38428  dihglblem2N  38432  dihglblem3N  38433  dihglbcpreN  38438  dihmeetlem3N  38443  dihjatc1  38449  dihjatc2N  38450  dihjatc3  38451  dihmeetlem15N  38459  infleinf  41647  mullimc  41904  mullimcf  41911  limsupre  41929  addlimc  41936  limclner  41939  sge0xaddlem2  42723  itscnhlc0xyqsol  44759  itsclquadb  44770  itsclquadeu  44771