Theorem simp11l 1277

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

Assertion

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

Proof of Theorem simp11l

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

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

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 1082

This theorem is referenced by:  pceu  16017  maduf  20939  lshpsmreu  35801  exatleN  36096  2llnjaN  36258  2lplnja  36311  dalemkehl  36315  dath2  36429  pclfinN  36592  lhp2lt  36693  lhpexle3lem  36703  lhpmcvr5N  36719  lhpmcvr6N  36720  lhp2at0  36724  lhp2atnle  36725  lhp2atne  36726  lhp2at0nle  36727  lhp2at0ne  36728  4atexlemk  36739  4atexlemex6  36766  4atexlem7  36767  cdlemd2  36891  cdlemd4  36893  cdlemd7  36896  cdleme0ex2N  36916  cdleme7aa  36934  cdleme7c  36937  cdleme7d  36938  cdleme7e  36939  cdleme7ga  36940  cdleme7  36941  cdleme11c  36953  cdleme11dN  36954  cdleme11e  36955  cdleme11  36962  cdleme14  36965  cdleme15a  36966  cdleme15b  36967  cdleme15c  36968  cdleme15d  36969  cdleme15  36970  cdleme16b  36971  cdleme16c  36972  cdleme16d  36973  cdleme16e  36974  cdleme16f  36975  cdleme18d  36987  cdleme19b  36996  cdleme19d  36998  cdleme19e  36999  cdleme20d  37004  cdleme20e  37005  cdleme20f  37006  cdleme20g  37007  cdleme20h  37008  cdleme20j  37010  cdleme20k  37011  cdleme20l1  37012  cdleme20l2  37013  cdleme20l  37014  cdleme20m  37015  cdleme21c  37019  cdleme21ct  37021  cdleme21d  37022  cdleme21e  37023  cdleme22cN  37034  cdleme22f  37038  cdleme22f2  37039  cdleme22g  37040  cdleme23a  37041  cdleme23b  37042  cdleme23c  37043  cdleme25a  37045  cdleme25c  37047  cdleme25dN  37048  cdleme26ee  37052  cdleme26eALTN  37053  cdleme27a  37059  cdleme27N  37061  cdleme28a  37062  cdleme28b  37063  cdleme29ex  37066  cdlemefrs29bpre0  37088  cdlemefrs29cpre1  37090  cdlemefr29exN  37094  cdleme32fva  37129  cdleme32b  37134  cdleme32c  37135  cdleme32e  37137  cdleme35a  37140  cdleme35fnpq  37141  cdleme35b  37142  cdleme35c  37143  cdleme35d  37144  cdleme35e  37145  cdleme35f  37146  cdleme36a  37152  cdleme37m  37154  cdleme39a  37157  cdleme42e  37171  cdleme42h  37174  cdleme42i  37175  cdleme42k  37176  cdleme43bN  37182  cdleme43dN  37184  cdleme17d2  37187  cdleme48bw  37194  cdlemeg46c  37205  cdlemeg46nlpq  37209  cdlemeg46ngfr  37210  cdlemeg46frv  37217  cdlemeg46vrg  37219  cdlemeg46rgv  37220  cdlemeg46req  37221  cdlemeg46gfv  37222  cdlemf1  37253  trlord  37261  cdlemb3  37298  cdlemg7fvbwN  37299  cdlemg10a  37332  cdlemg10  37333  cdlemg12e  37339  cdlemg12f  37340  cdlemg12g  37341  cdlemg12  37342  cdlemg13a  37343  cdlemg13  37344  cdlemg17b  37354  cdlemg17g  37359  cdlemg17h  37360  cdlemg17pq  37364  cdlemg17  37369  cdlemg19a  37375  cdlemg19  37376  cdlemg21  37378  cdlemg27a  37384  cdlemg27b  37388  cdlemg31c  37391  cdlemg33b0  37393  cdlemg33c0  37394  cdlemg33a  37398  cdlemg33c  37400  cdlemg33e  37402  cdlemg35  37405  trlcone  37420  tendococl  37464  cdlemh1  37507  cdlemh2  37508  cdlemh  37509  cdlemi  37512  cdlemk5  37528  cdlemk6  37529  cdlemki  37533  cdlemksv2  37539  cdlemk7  37540  cdlemk11  37541  cdlemk12  37542  cdlemkole  37545  cdlemk14  37546  cdlemk15  37547  cdlemk17  37550  cdlemk1u  37551  cdlemk5u  37553  cdlemk6u  37554  cdlemkj  37555  cdlemkuv2  37559  cdlemk7u  37562  cdlemk11u  37563  cdlemk12u  37564  cdlemk26-3  37598  cdlemk37  37606  cdlemk11t  37638  cdlemk47  37641  cdlemk48  37642  cdlemk50  37644  cdlemk51  37645  cdlemk52  37646  cdlemk53a  37647  cdlemk39u  37660  dihord1  37910  dihord2a  37911  dihord2b  37912  dihord11b  37914  dihord11c  37916  dihord2pre  37917  dihord2pre2  37918  dihord5apre  37954  dihmeetlem1N  37982  dihglblem2N  37986  dihglblem3N  37987  dihglbcpreN  37992  dihmeetlem3N  37997  dihjatc1  38003  dihjatc2N  38004  dihjatc3  38005  dihmeetlem15N  38013  infleinf  41206  mullimc  41464  mullimcf  41471  limsupre  41489  addlimc  41496  limclner  41499  sge0xaddlem2  42284  itscnhlc0xyqsol  44259  itsclquadb  44270  itsclquadeu  44271