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  16786  maduf  22597  lshpsmreu  39479  exatleN  39774  2llnjaN  39936  2lplnja  39989  dalemkehl  39993  dath2  40107  pclfinN  40270  lhp2lt  40371  lhpexle3lem  40381  lhpmcvr5N  40397  lhpmcvr6N  40398  lhp2at0  40402  lhp2atnle  40403  lhp2atne  40404  lhp2at0nle  40405  lhp2at0ne  40406  4atexlemk  40417  4atexlemex6  40444  4atexlem7  40445  cdlemd2  40569  cdlemd4  40571  cdlemd7  40574  cdleme0ex2N  40594  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme11c  40631  cdleme11dN  40632  cdleme11e  40633  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15b  40645  cdleme15c  40646  cdleme15d  40647  cdleme15  40648  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme18d  40665  cdleme19b  40674  cdleme19d  40676  cdleme19e  40677  cdleme20d  40682  cdleme20e  40683  cdleme20f  40684  cdleme20g  40685  cdleme20h  40686  cdleme20j  40688  cdleme20k  40689  cdleme20l1  40690  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21c  40697  cdleme21ct  40699  cdleme21d  40700  cdleme21e  40701  cdleme22cN  40712  cdleme22f  40716  cdleme22f2  40717  cdleme22g  40718  cdleme23a  40719  cdleme23b  40720  cdleme23c  40721  cdleme25a  40723  cdleme25c  40725  cdleme25dN  40726  cdleme26ee  40730  cdleme26eALTN  40731  cdleme27a  40737  cdleme27N  40739  cdleme28a  40740  cdleme28b  40741  cdleme29ex  40744  cdlemefrs29bpre0  40766  cdlemefrs29cpre1  40768  cdlemefr29exN  40772  cdleme32fva  40807  cdleme32b  40812  cdleme32c  40813  cdleme32e  40815  cdleme35a  40818  cdleme35fnpq  40819  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35e  40823  cdleme35f  40824  cdleme36a  40830  cdleme37m  40832  cdleme39a  40835  cdleme42e  40849  cdleme42h  40852  cdleme42i  40853  cdleme42k  40854  cdleme43bN  40860  cdleme43dN  40862  cdleme17d2  40865  cdleme48bw  40872  cdlemeg46c  40883  cdlemeg46nlpq  40887  cdlemeg46ngfr  40888  cdlemeg46frv  40895  cdlemeg46vrg  40897  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemeg46gfv  40900  cdlemf1  40931  trlord  40939  cdlemb3  40976  cdlemg7fvbwN  40977  cdlemg10a  41010  cdlemg10  41011  cdlemg12e  41017  cdlemg12f  41018  cdlemg12g  41019  cdlemg12  41020  cdlemg13a  41021  cdlemg13  41022  cdlemg17b  41032  cdlemg17g  41037  cdlemg17h  41038  cdlemg17pq  41042  cdlemg17  41047  cdlemg19a  41053  cdlemg19  41054  cdlemg21  41056  cdlemg27a  41062  cdlemg27b  41066  cdlemg31c  41069  cdlemg33b0  41071  cdlemg33c0  41072  cdlemg33a  41076  cdlemg33c  41078  cdlemg33e  41080  cdlemg35  41083  trlcone  41098  tendococl  41142  cdlemh1  41185  cdlemh2  41186  cdlemh  41187  cdlemi  41190  cdlemk5  41206  cdlemk6  41207  cdlemki  41211  cdlemksv2  41217  cdlemk7  41218  cdlemk11  41219  cdlemk12  41220  cdlemkole  41223  cdlemk14  41224  cdlemk15  41225  cdlemk17  41228  cdlemk1u  41229  cdlemk5u  41231  cdlemk6u  41232  cdlemkj  41233  cdlemkuv2  41237  cdlemk7u  41240  cdlemk11u  41241  cdlemk12u  41242  cdlemk26-3  41276  cdlemk37  41284  cdlemk11t  41316  cdlemk47  41319  cdlemk48  41320  cdlemk50  41322  cdlemk51  41323  cdlemk52  41324  cdlemk53a  41325  cdlemk39u  41338  dihord1  41588  dihord2a  41589  dihord2b  41590  dihord11b  41592  dihord11c  41594  dihord2pre  41595  dihord2pre2  41596  dihord5apre  41632  dihmeetlem1N  41660  dihglblem2N  41664  dihglblem3N  41665  dihglbcpreN  41670  dihmeetlem3N  41675  dihjatc1  41681  dihjatc2N  41682  dihjatc3  41683  dihmeetlem15N  41691  infleinf  45724  mullimc  45970  mullimcf  45977  limsupre  45993  addlimc  46000  limclner  46003  sge0xaddlem2  46786  itscnhlc0xyqsol  49119  itsclquadb  49130  itsclquadeu  49131