Theorem simp11l 1303

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

Assertion

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

Proof of Theorem simp11l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  17056  maduf  22989  lshpsmreu  40369  exatleN  40664  2llnjaN  40826  2lplnja  40879  dalemkehl  40883  dath2  40997  pclfinN  41160  lhp2lt  41261  lhpexle3lem  41271  lhpmcvr5N  41287  lhpmcvr6N  41288  lhp2at0  41292  lhp2atnle  41293  lhp2atne  41294  lhp2at0nle  41295  lhp2at0ne  41296  4atexlemk  41307  4atexlemex6  41334  4atexlem7  41335  cdlemd2  41459  cdlemd4  41461  cdlemd7  41464  cdleme0ex2N  41484  cdleme7aa  41502  cdleme7c  41505  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme11c  41521  cdleme11dN  41522  cdleme11e  41523  cdleme11  41530  cdleme14  41533  cdleme15a  41534  cdleme15b  41535  cdleme15c  41536  cdleme15d  41537  cdleme15  41538  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme16e  41542  cdleme16f  41543  cdleme18d  41555  cdleme19b  41564  cdleme19d  41566  cdleme19e  41567  cdleme20d  41572  cdleme20e  41573  cdleme20f  41574  cdleme20g  41575  cdleme20h  41576  cdleme20j  41578  cdleme20k  41579  cdleme20l1  41580  cdleme20l2  41581  cdleme20l  41582  cdleme20m  41583  cdleme21c  41587  cdleme21ct  41589  cdleme21d  41590  cdleme21e  41591  cdleme22cN  41602  cdleme22f  41606  cdleme22f2  41607  cdleme22g  41608  cdleme23a  41609  cdleme23b  41610  cdleme23c  41611  cdleme25a  41613  cdleme25c  41615  cdleme25dN  41616  cdleme26ee  41620  cdleme26eALTN  41621  cdleme27a  41627  cdleme27N  41629  cdleme28a  41630  cdleme28b  41631  cdleme29ex  41634  cdlemefrs29bpre0  41656  cdlemefrs29cpre1  41658  cdlemefr29exN  41662  cdleme32fva  41697  cdleme32b  41702  cdleme32c  41703  cdleme32e  41705  cdleme35a  41708  cdleme35fnpq  41709  cdleme35b  41710  cdleme35c  41711  cdleme35d  41712  cdleme35e  41713  cdleme35f  41714  cdleme36a  41720  cdleme37m  41722  cdleme39a  41725  cdleme42e  41739  cdleme42h  41742  cdleme42i  41743  cdleme42k  41744  cdleme43bN  41750  cdleme43dN  41752  cdleme17d2  41755  cdleme48bw  41762  cdlemeg46c  41773  cdlemeg46nlpq  41777  cdlemeg46ngfr  41778  cdlemeg46frv  41785  cdlemeg46vrg  41787  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemeg46gfv  41790  cdlemf1  41821  trlord  41829  cdlemb3  41866  cdlemg7fvbwN  41867  cdlemg10a  41900  cdlemg10  41901  cdlemg12e  41907  cdlemg12f  41908  cdlemg12g  41909  cdlemg12  41910  cdlemg13a  41911  cdlemg13  41912  cdlemg17b  41922  cdlemg17g  41927  cdlemg17h  41928  cdlemg17pq  41932  cdlemg17  41937  cdlemg19a  41943  cdlemg19  41944  cdlemg21  41946  cdlemg27a  41952  cdlemg27b  41956  cdlemg31c  41959  cdlemg33b0  41961  cdlemg33c0  41962  cdlemg33a  41966  cdlemg33c  41968  cdlemg33e  41970  cdlemg35  41973  trlcone  41988  tendococl  42032  cdlemh1  42075  cdlemh2  42076  cdlemh  42077  cdlemi  42080  cdlemk5  42096  cdlemk6  42097  cdlemki  42101  cdlemksv2  42107  cdlemk7  42108  cdlemk11  42109  cdlemk12  42110  cdlemkole  42113  cdlemk14  42114  cdlemk15  42115  cdlemk17  42118  cdlemk1u  42119  cdlemk5u  42121  cdlemk6u  42122  cdlemkj  42123  cdlemkuv2  42127  cdlemk7u  42130  cdlemk11u  42131  cdlemk12u  42132  cdlemk26-3  42166  cdlemk37  42174  cdlemk11t  42206  cdlemk47  42209  cdlemk48  42210  cdlemk50  42212  cdlemk51  42213  cdlemk52  42214  cdlemk53a  42215  cdlemk39u  42228  dihord1  42478  dihord2a  42479  dihord2b  42480  dihord11b  42482  dihord11c  42484  dihord2pre  42485  dihord2pre2  42486  dihord5apre  42522  dihmeetlem1N  42550  dihglblem2N  42554  dihglblem3N  42555  dihglbcpreN  42560  dihmeetlem3N  42565  dihjatc1  42571  dihjatc2N  42572  dihjatc3  42573  dihmeetlem15N  42581  infleinf  46598  mullimc  46843  mullimcf  46850  limsupre  46866  addlimc  46873  limclner  46876  sge0xaddlem2  47659  itscnhlc0xyqsol  50092  itsclquadb  50103  itsclquadeu  50104