Theorem simp11l 1281

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  pceu  16822  maduf  22563  lshpsmreu  38613  exatleN  38909  2llnjaN  39071  2lplnja  39124  dalemkehl  39128  dath2  39242  pclfinN  39405  lhp2lt  39506  lhpexle3lem  39516  lhpmcvr5N  39532  lhpmcvr6N  39533  lhp2at0  39537  lhp2atnle  39538  lhp2atne  39539  lhp2at0nle  39540  lhp2at0ne  39541  4atexlemk  39552  4atexlemex6  39579  4atexlem7  39580  cdlemd2  39704  cdlemd4  39706  cdlemd7  39709  cdleme0ex2N  39729  cdleme7aa  39747  cdleme7c  39750  cdleme7d  39751  cdleme7e  39752  cdleme7ga  39753  cdleme7  39754  cdleme11c  39766  cdleme11dN  39767  cdleme11e  39768  cdleme11  39775  cdleme14  39778  cdleme15a  39779  cdleme15b  39780  cdleme15c  39781  cdleme15d  39782  cdleme15  39783  cdleme16b  39784  cdleme16c  39785  cdleme16d  39786  cdleme16e  39787  cdleme16f  39788  cdleme18d  39800  cdleme19b  39809  cdleme19d  39811  cdleme19e  39812  cdleme20d  39817  cdleme20e  39818  cdleme20f  39819  cdleme20g  39820  cdleme20h  39821  cdleme20j  39823  cdleme20k  39824  cdleme20l1  39825  cdleme20l2  39826  cdleme20l  39827  cdleme20m  39828  cdleme21c  39832  cdleme21ct  39834  cdleme21d  39835  cdleme21e  39836  cdleme22cN  39847  cdleme22f  39851  cdleme22f2  39852  cdleme22g  39853  cdleme23a  39854  cdleme23b  39855  cdleme23c  39856  cdleme25a  39858  cdleme25c  39860  cdleme25dN  39861  cdleme26ee  39865  cdleme26eALTN  39866  cdleme27a  39872  cdleme27N  39874  cdleme28a  39875  cdleme28b  39876  cdleme29ex  39879  cdlemefrs29bpre0  39901  cdlemefrs29cpre1  39903  cdlemefr29exN  39907  cdleme32fva  39942  cdleme32b  39947  cdleme32c  39948  cdleme32e  39950  cdleme35a  39953  cdleme35fnpq  39954  cdleme35b  39955  cdleme35c  39956  cdleme35d  39957  cdleme35e  39958  cdleme35f  39959  cdleme36a  39965  cdleme37m  39967  cdleme39a  39970  cdleme42e  39984  cdleme42h  39987  cdleme42i  39988  cdleme42k  39989  cdleme43bN  39995  cdleme43dN  39997  cdleme17d2  40000  cdleme48bw  40007  cdlemeg46c  40018  cdlemeg46nlpq  40022  cdlemeg46ngfr  40023  cdlemeg46frv  40030  cdlemeg46vrg  40032  cdlemeg46rgv  40033  cdlemeg46req  40034  cdlemeg46gfv  40035  cdlemf1  40066  trlord  40074  cdlemb3  40111  cdlemg7fvbwN  40112  cdlemg10a  40145  cdlemg10  40146  cdlemg12e  40152  cdlemg12f  40153  cdlemg12g  40154  cdlemg12  40155  cdlemg13a  40156  cdlemg13  40157  cdlemg17b  40167  cdlemg17g  40172  cdlemg17h  40173  cdlemg17pq  40177  cdlemg17  40182  cdlemg19a  40188  cdlemg19  40189  cdlemg21  40191  cdlemg27a  40197  cdlemg27b  40201  cdlemg31c  40204  cdlemg33b0  40206  cdlemg33c0  40207  cdlemg33a  40211  cdlemg33c  40213  cdlemg33e  40215  cdlemg35  40218  trlcone  40233  tendococl  40277  cdlemh1  40320  cdlemh2  40321  cdlemh  40322  cdlemi  40325  cdlemk5  40341  cdlemk6  40342  cdlemki  40346  cdlemksv2  40352  cdlemk7  40353  cdlemk11  40354  cdlemk12  40355  cdlemkole  40358  cdlemk14  40359  cdlemk15  40360  cdlemk17  40363  cdlemk1u  40364  cdlemk5u  40366  cdlemk6u  40367  cdlemkj  40368  cdlemkuv2  40372  cdlemk7u  40375  cdlemk11u  40376  cdlemk12u  40377  cdlemk26-3  40411  cdlemk37  40419  cdlemk11t  40451  cdlemk47  40454  cdlemk48  40455  cdlemk50  40457  cdlemk51  40458  cdlemk52  40459  cdlemk53a  40460  cdlemk39u  40473  dihord1  40723  dihord2a  40724  dihord2b  40725  dihord11b  40727  dihord11c  40729  dihord2pre  40730  dihord2pre2  40731  dihord5apre  40767  dihmeetlem1N  40795  dihglblem2N  40799  dihglblem3N  40800  dihglbcpreN  40805  dihmeetlem3N  40810  dihjatc1  40816  dihjatc2N  40817  dihjatc3  40818  dihmeetlem15N  40826  infleinf  44783  mullimc  45033  mullimcf  45040  limsupre  45058  addlimc  45065  limclner  45068  sge0xaddlem2  45851  itscnhlc0xyqsol  47916  itsclquadb  47927  itsclquadeu  47928