Theorem simp11l 1286

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pceu  16808  maduf  22616  lshpsmreu  39569  exatleN  39864  2llnjaN  40026  2lplnja  40079  dalemkehl  40083  dath2  40197  pclfinN  40360  lhp2lt  40461  lhpexle3lem  40471  lhpmcvr5N  40487  lhpmcvr6N  40488  lhp2at0  40492  lhp2atnle  40493  lhp2atne  40494  lhp2at0nle  40495  lhp2at0ne  40496  4atexlemk  40507  4atexlemex6  40534  4atexlem7  40535  cdlemd2  40659  cdlemd4  40661  cdlemd7  40664  cdleme0ex2N  40684  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme11c  40721  cdleme11dN  40722  cdleme11e  40723  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme15b  40735  cdleme15c  40736  cdleme15d  40737  cdleme15  40738  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme18d  40755  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20d  40772  cdleme20e  40773  cdleme20f  40774  cdleme20g  40775  cdleme20h  40776  cdleme20j  40778  cdleme20k  40779  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21c  40787  cdleme21ct  40789  cdleme21d  40790  cdleme21e  40791  cdleme22cN  40802  cdleme22f  40806  cdleme22f2  40807  cdleme22g  40808  cdleme23a  40809  cdleme23b  40810  cdleme23c  40811  cdleme25a  40813  cdleme25c  40815  cdleme25dN  40816  cdleme26ee  40820  cdleme26eALTN  40821  cdleme27a  40827  cdleme27N  40829  cdleme28a  40830  cdleme28b  40831  cdleme29ex  40834  cdlemefrs29bpre0  40856  cdlemefrs29cpre1  40858  cdlemefr29exN  40862  cdleme32fva  40897  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme35f  40914  cdleme36a  40920  cdleme37m  40922  cdleme39a  40925  cdleme42e  40939  cdleme42h  40942  cdleme42i  40943  cdleme42k  40944  cdleme43bN  40950  cdleme43dN  40952  cdleme17d2  40955  cdleme48bw  40962  cdlemeg46c  40973  cdlemeg46nlpq  40977  cdlemeg46ngfr  40978  cdlemeg46frv  40985  cdlemeg46vrg  40987  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdlemf1  41021  trlord  41029  cdlemb3  41066  cdlemg7fvbwN  41067  cdlemg10a  41100  cdlemg10  41101  cdlemg12e  41107  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg13a  41111  cdlemg13  41112  cdlemg17b  41122  cdlemg17g  41127  cdlemg17h  41128  cdlemg17pq  41132  cdlemg17  41137  cdlemg19a  41143  cdlemg19  41144  cdlemg21  41146  cdlemg27a  41152  cdlemg27b  41156  cdlemg31c  41159  cdlemg33b0  41161  cdlemg33c0  41162  cdlemg33a  41166  cdlemg33c  41168  cdlemg33e  41170  cdlemg35  41173  trlcone  41188  tendococl  41232  cdlemh1  41275  cdlemh2  41276  cdlemh  41277  cdlemi  41280  cdlemk5  41296  cdlemk6  41297  cdlemki  41301  cdlemksv2  41307  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemkole  41313  cdlemk14  41314  cdlemk15  41315  cdlemk17  41318  cdlemk1u  41319  cdlemk5u  41321  cdlemk6u  41322  cdlemkj  41323  cdlemkuv2  41327  cdlemk7u  41330  cdlemk11u  41331  cdlemk12u  41332  cdlemk26-3  41366  cdlemk37  41374  cdlemk11t  41406  cdlemk47  41409  cdlemk48  41410  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  cdlemk53a  41415  cdlemk39u  41428  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord11b  41682  dihord11c  41684  dihord2pre  41685  dihord2pre2  41686  dihord5apre  41722  dihmeetlem1N  41750  dihglblem2N  41754  dihglblem3N  41755  dihglbcpreN  41760  dihmeetlem3N  41765  dihjatc1  41771  dihjatc2N  41772  dihjatc3  41773  dihmeetlem15N  41781  infleinf  45819  mullimc  46064  mullimcf  46071  limsupre  46087  addlimc  46094  limclner  46097  sge0xaddlem2  46880  itscnhlc0xyqsol  49253  itsclquadb  49264  itsclquadeu  49265