Theorem simp11l 1376

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  pceu  15762  maduf  20652  lshpsmreu  34883  exatleN  35178  2llnjaN  35340  2lplnja  35393  dalemkehl  35397  dath2  35511  pclfinN  35674  lhp2lt  35775  lhpexle3lem  35785  lhpmcvr5N  35801  lhpmcvr6N  35802  lhp2at0  35806  lhp2atnle  35807  lhp2atne  35808  lhp2at0nle  35809  lhp2at0ne  35810  4atexlemk  35821  4atexlemex6  35848  4atexlem7  35849  cdlemd2  35974  cdlemd4  35976  cdlemd7  35979  cdleme0ex2N  35999  cdleme7aa  36017  cdleme7c  36020  cdleme7d  36021  cdleme7e  36022  cdleme7ga  36023  cdleme7  36024  cdleme11c  36036  cdleme11dN  36037  cdleme11e  36038  cdleme11  36045  cdleme14  36048  cdleme15a  36049  cdleme15b  36050  cdleme15c  36051  cdleme15d  36052  cdleme15  36053  cdleme16b  36054  cdleme16c  36055  cdleme16d  36056  cdleme16e  36057  cdleme16f  36058  cdleme18d  36070  cdleme19b  36079  cdleme19d  36081  cdleme19e  36082  cdleme20d  36087  cdleme20e  36088  cdleme20f  36089  cdleme20g  36090  cdleme20h  36091  cdleme20j  36093  cdleme20k  36094  cdleme20l1  36095  cdleme20l2  36096  cdleme20l  36097  cdleme20m  36098  cdleme21c  36102  cdleme21ct  36104  cdleme21d  36105  cdleme21e  36106  cdleme22cN  36117  cdleme22f  36121  cdleme22f2  36122  cdleme22g  36123  cdleme23a  36124  cdleme23b  36125  cdleme23c  36126  cdleme25a  36128  cdleme25c  36130  cdleme25dN  36131  cdleme26ee  36135  cdleme26eALTN  36136  cdleme27a  36142  cdleme27N  36144  cdleme28a  36145  cdleme28b  36146  cdleme29ex  36149  cdlemefrs29bpre0  36171  cdlemefrs29cpre1  36173  cdlemefr29exN  36177  cdleme32fva  36212  cdleme32b  36217  cdleme32c  36218  cdleme32e  36220  cdleme35a  36223  cdleme35fnpq  36224  cdleme35b  36225  cdleme35c  36226  cdleme35d  36227  cdleme35e  36228  cdleme35f  36229  cdleme36a  36235  cdleme37m  36237  cdleme39a  36240  cdleme42e  36254  cdleme42h  36257  cdleme42i  36258  cdleme42k  36259  cdleme43bN  36265  cdleme43dN  36267  cdleme17d2  36270  cdleme48bw  36277  cdlemeg46c  36288  cdlemeg46nlpq  36292  cdlemeg46ngfr  36293  cdlemeg46frv  36300  cdlemeg46vrg  36302  cdlemeg46rgv  36303  cdlemeg46req  36304  cdlemeg46gfv  36305  cdlemf1  36336  trlord  36344  cdlemb3  36381  cdlemg7fvbwN  36382  cdlemg10a  36415  cdlemg10  36416  cdlemg12e  36422  cdlemg12f  36423  cdlemg12g  36424  cdlemg12  36425  cdlemg13a  36426  cdlemg13  36427  cdlemg17b  36437  cdlemg17g  36442  cdlemg17h  36443  cdlemg17pq  36447  cdlemg17  36452  cdlemg19a  36458  cdlemg19  36459  cdlemg21  36461  cdlemg27a  36467  cdlemg27b  36471  cdlemg31c  36474  cdlemg33b0  36476  cdlemg33c0  36477  cdlemg33a  36481  cdlemg33c  36483  cdlemg33e  36485  cdlemg35  36488  trlcone  36503  tendococl  36547  cdlemh1  36590  cdlemh2  36591  cdlemh  36592  cdlemi  36595  cdlemk5  36611  cdlemk6  36612  cdlemki  36616  cdlemksv2  36622  cdlemk7  36623  cdlemk11  36624  cdlemk12  36625  cdlemkole  36628  cdlemk14  36629  cdlemk15  36630  cdlemk17  36633  cdlemk1u  36634  cdlemk5u  36636  cdlemk6u  36637  cdlemkj  36638  cdlemkuv2  36642  cdlemk7u  36645  cdlemk11u  36646  cdlemk12u  36647  cdlemk26-3  36681  cdlemk37  36689  cdlemk11t  36721  cdlemk47  36724  cdlemk48  36725  cdlemk50  36727  cdlemk51  36728  cdlemk52  36729  cdlemk53a  36730  cdlemk39u  36743  dihord1  36993  dihord2a  36994  dihord2b  36995  dihord11b  36997  dihord11c  36999  dihord2pre  37000  dihord2pre2  37001  dihord5apre  37037  dihmeetlem1N  37065  dihglblem2N  37069  dihglblem3N  37070  dihglbcpreN  37075  dihmeetlem3N  37080  dihjatc1  37086  dihjatc2N  37087  dihjatc3  37088  dihmeetlem15N  37096  infleinf  40062  mullimc  40322  mullimcf  40329  limsupre  40347  addlimc  40354  limclner  40357  sge0xaddlem2  41124