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  16760  maduf  22557  lshpsmreu  39228  exatleN  39523  2llnjaN  39685  2lplnja  39738  dalemkehl  39742  dath2  39856  pclfinN  40019  lhp2lt  40120  lhpexle3lem  40130  lhpmcvr5N  40146  lhpmcvr6N  40147  lhp2at0  40151  lhp2atnle  40152  lhp2atne  40153  lhp2at0nle  40154  lhp2at0ne  40155  4atexlemk  40166  4atexlemex6  40193  4atexlem7  40194  cdlemd2  40318  cdlemd4  40320  cdlemd7  40323  cdleme0ex2N  40343  cdleme7aa  40361  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme11c  40380  cdleme11dN  40381  cdleme11e  40382  cdleme11  40389  cdleme14  40392  cdleme15a  40393  cdleme15b  40394  cdleme15c  40395  cdleme15d  40396  cdleme15  40397  cdleme16b  40398  cdleme16c  40399  cdleme16d  40400  cdleme16e  40401  cdleme16f  40402  cdleme18d  40414  cdleme19b  40423  cdleme19d  40425  cdleme19e  40426  cdleme20d  40431  cdleme20e  40432  cdleme20f  40433  cdleme20g  40434  cdleme20h  40435  cdleme20j  40437  cdleme20k  40438  cdleme20l1  40439  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21c  40446  cdleme21ct  40448  cdleme21d  40449  cdleme21e  40450  cdleme22cN  40461  cdleme22f  40465  cdleme22f2  40466  cdleme22g  40467  cdleme23a  40468  cdleme23b  40469  cdleme23c  40470  cdleme25a  40472  cdleme25c  40474  cdleme25dN  40475  cdleme26ee  40479  cdleme26eALTN  40480  cdleme27a  40486  cdleme27N  40488  cdleme28a  40489  cdleme28b  40490  cdleme29ex  40493  cdlemefrs29bpre0  40515  cdlemefrs29cpre1  40517  cdlemefr29exN  40521  cdleme32fva  40556  cdleme32b  40561  cdleme32c  40562  cdleme32e  40564  cdleme35a  40567  cdleme35fnpq  40568  cdleme35b  40569  cdleme35c  40570  cdleme35d  40571  cdleme35e  40572  cdleme35f  40573  cdleme36a  40579  cdleme37m  40581  cdleme39a  40584  cdleme42e  40598  cdleme42h  40601  cdleme42i  40602  cdleme42k  40603  cdleme43bN  40609  cdleme43dN  40611  cdleme17d2  40614  cdleme48bw  40621  cdlemeg46c  40632  cdlemeg46nlpq  40636  cdlemeg46ngfr  40637  cdlemeg46frv  40644  cdlemeg46vrg  40646  cdlemeg46rgv  40647  cdlemeg46req  40648  cdlemeg46gfv  40649  cdlemf1  40680  trlord  40688  cdlemb3  40725  cdlemg7fvbwN  40726  cdlemg10a  40759  cdlemg10  40760  cdlemg12e  40766  cdlemg12f  40767  cdlemg12g  40768  cdlemg12  40769  cdlemg13a  40770  cdlemg13  40771  cdlemg17b  40781  cdlemg17g  40786  cdlemg17h  40787  cdlemg17pq  40791  cdlemg17  40796  cdlemg19a  40802  cdlemg19  40803  cdlemg21  40805  cdlemg27a  40811  cdlemg27b  40815  cdlemg31c  40818  cdlemg33b0  40820  cdlemg33c0  40821  cdlemg33a  40825  cdlemg33c  40827  cdlemg33e  40829  cdlemg35  40832  trlcone  40847  tendococl  40891  cdlemh1  40934  cdlemh2  40935  cdlemh  40936  cdlemi  40939  cdlemk5  40955  cdlemk6  40956  cdlemki  40960  cdlemksv2  40966  cdlemk7  40967  cdlemk11  40968  cdlemk12  40969  cdlemkole  40972  cdlemk14  40973  cdlemk15  40974  cdlemk17  40977  cdlemk1u  40978  cdlemk5u  40980  cdlemk6u  40981  cdlemkj  40982  cdlemkuv2  40986  cdlemk7u  40989  cdlemk11u  40990  cdlemk12u  40991  cdlemk26-3  41025  cdlemk37  41033  cdlemk11t  41065  cdlemk47  41068  cdlemk48  41069  cdlemk50  41071  cdlemk51  41072  cdlemk52  41073  cdlemk53a  41074  cdlemk39u  41087  dihord1  41337  dihord2a  41338  dihord2b  41339  dihord11b  41341  dihord11c  41343  dihord2pre  41344  dihord2pre2  41345  dihord5apre  41381  dihmeetlem1N  41409  dihglblem2N  41413  dihglblem3N  41414  dihglbcpreN  41419  dihmeetlem3N  41424  dihjatc1  41430  dihjatc2N  41431  dihjatc3  41432  dihmeetlem15N  41440  infleinf  45494  mullimc  45740  mullimcf  45747  limsupre  45763  addlimc  45770  limclner  45773  sge0xaddlem2  46556  itscnhlc0xyqsol  48890  itsclquadb  48901  itsclquadeu  48902