Theorem simp11l 1285

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

Assertion

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

Proof of Theorem simp11l

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

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

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 1088

This theorem is referenced by:  pceu  16824  maduf  22535  lshpsmreu  39109  exatleN  39405  2llnjaN  39567  2lplnja  39620  dalemkehl  39624  dath2  39738  pclfinN  39901  lhp2lt  40002  lhpexle3lem  40012  lhpmcvr5N  40028  lhpmcvr6N  40029  lhp2at0  40033  lhp2atnle  40034  lhp2atne  40035  lhp2at0nle  40036  lhp2at0ne  40037  4atexlemk  40048  4atexlemex6  40075  4atexlem7  40076  cdlemd2  40200  cdlemd4  40202  cdlemd7  40205  cdleme0ex2N  40225  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme11c  40262  cdleme11dN  40263  cdleme11e  40264  cdleme11  40271  cdleme14  40274  cdleme15a  40275  cdleme15b  40276  cdleme15c  40277  cdleme15d  40278  cdleme15  40279  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme18d  40296  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20d  40313  cdleme20e  40314  cdleme20f  40315  cdleme20g  40316  cdleme20h  40317  cdleme20j  40319  cdleme20k  40320  cdleme20l1  40321  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21c  40328  cdleme21ct  40330  cdleme21d  40331  cdleme21e  40332  cdleme22cN  40343  cdleme22f  40347  cdleme22f2  40348  cdleme22g  40349  cdleme23a  40350  cdleme23b  40351  cdleme23c  40352  cdleme25a  40354  cdleme25c  40356  cdleme25dN  40357  cdleme26ee  40361  cdleme26eALTN  40362  cdleme27a  40368  cdleme27N  40370  cdleme28a  40371  cdleme28b  40372  cdleme29ex  40375  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdlemefr29exN  40403  cdleme32fva  40438  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35e  40454  cdleme35f  40455  cdleme36a  40461  cdleme37m  40463  cdleme39a  40466  cdleme42e  40480  cdleme42h  40483  cdleme42i  40484  cdleme42k  40485  cdleme43bN  40491  cdleme43dN  40493  cdleme17d2  40496  cdleme48bw  40503  cdlemeg46c  40514  cdlemeg46nlpq  40518  cdlemeg46ngfr  40519  cdlemeg46frv  40526  cdlemeg46vrg  40528  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfv  40531  cdlemf1  40562  trlord  40570  cdlemb3  40607  cdlemg7fvbwN  40608  cdlemg10a  40641  cdlemg10  40642  cdlemg12e  40648  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg13a  40652  cdlemg13  40653  cdlemg17b  40663  cdlemg17g  40668  cdlemg17h  40669  cdlemg17pq  40673  cdlemg17  40678  cdlemg19a  40684  cdlemg19  40685  cdlemg21  40687  cdlemg27a  40693  cdlemg27b  40697  cdlemg31c  40700  cdlemg33b0  40702  cdlemg33c0  40703  cdlemg33a  40707  cdlemg33c  40709  cdlemg33e  40711  cdlemg35  40714  trlcone  40729  tendococl  40773  cdlemh1  40816  cdlemh2  40817  cdlemh  40818  cdlemi  40821  cdlemk5  40837  cdlemk6  40838  cdlemki  40842  cdlemksv2  40848  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemkole  40854  cdlemk14  40855  cdlemk15  40856  cdlemk17  40859  cdlemk1u  40860  cdlemk5u  40862  cdlemk6u  40863  cdlemkj  40864  cdlemkuv2  40868  cdlemk7u  40871  cdlemk11u  40872  cdlemk12u  40873  cdlemk26-3  40907  cdlemk37  40915  cdlemk11t  40947  cdlemk47  40950  cdlemk48  40951  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk53a  40956  cdlemk39u  40969  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord11b  41223  dihord11c  41225  dihord2pre  41226  dihord2pre2  41227  dihord5apre  41263  dihmeetlem1N  41291  dihglblem2N  41295  dihglblem3N  41296  dihglbcpreN  41301  dihmeetlem3N  41306  dihjatc1  41312  dihjatc2N  41313  dihjatc3  41314  dihmeetlem15N  41322  infleinf  45375  mullimc  45621  mullimcf  45628  limsupre  45646  addlimc  45653  limclner  45656  sge0xaddlem2  46439  itscnhlc0xyqsol  48758  itsclquadb  48769  itsclquadeu  48770