Theorem simp11l 1282

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

Assertion

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

Proof of Theorem simp11l

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  pceu  16475  maduf  21698  lshpsmreu  37050  exatleN  37345  2llnjaN  37507  2lplnja  37560  dalemkehl  37564  dath2  37678  pclfinN  37841  lhp2lt  37942  lhpexle3lem  37952  lhpmcvr5N  37968  lhpmcvr6N  37969  lhp2at0  37973  lhp2atnle  37974  lhp2atne  37975  lhp2at0nle  37976  lhp2at0ne  37977  4atexlemk  37988  4atexlemex6  38015  4atexlem7  38016  cdlemd2  38140  cdlemd4  38142  cdlemd7  38145  cdleme0ex2N  38165  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme11c  38202  cdleme11dN  38203  cdleme11e  38204  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme15b  38216  cdleme15c  38217  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme18d  38236  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20d  38253  cdleme20e  38254  cdleme20f  38255  cdleme20g  38256  cdleme20h  38257  cdleme20j  38259  cdleme20k  38260  cdleme20l1  38261  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21c  38268  cdleme21ct  38270  cdleme21d  38271  cdleme21e  38272  cdleme22cN  38283  cdleme22f  38287  cdleme22f2  38288  cdleme22g  38289  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme25a  38294  cdleme25c  38296  cdleme25dN  38297  cdleme26ee  38301  cdleme26eALTN  38302  cdleme27a  38308  cdleme27N  38310  cdleme28a  38311  cdleme28b  38312  cdleme29ex  38315  cdlemefrs29bpre0  38337  cdlemefrs29cpre1  38339  cdlemefr29exN  38343  cdleme32fva  38378  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme36a  38401  cdleme37m  38403  cdleme39a  38406  cdleme42e  38420  cdleme42h  38423  cdleme42i  38424  cdleme42k  38425  cdleme43bN  38431  cdleme43dN  38433  cdleme17d2  38436  cdleme48bw  38443  cdlemeg46c  38454  cdlemeg46nlpq  38458  cdlemeg46ngfr  38459  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfv  38471  cdlemf1  38502  trlord  38510  cdlemb3  38547  cdlemg7fvbwN  38548  cdlemg10a  38581  cdlemg10  38582  cdlemg12e  38588  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg13  38593  cdlemg17b  38603  cdlemg17g  38608  cdlemg17h  38609  cdlemg17pq  38613  cdlemg17  38618  cdlemg19a  38624  cdlemg19  38625  cdlemg21  38627  cdlemg27a  38633  cdlemg27b  38637  cdlemg31c  38640  cdlemg33b0  38642  cdlemg33c0  38643  cdlemg33a  38647  cdlemg33c  38649  cdlemg33e  38651  cdlemg35  38654  trlcone  38669  tendococl  38713  cdlemh1  38756  cdlemh2  38757  cdlemh  38758  cdlemi  38761  cdlemk5  38777  cdlemk6  38778  cdlemki  38782  cdlemksv2  38788  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk17  38799  cdlemk1u  38800  cdlemk5u  38802  cdlemk6u  38803  cdlemkj  38804  cdlemkuv2  38808  cdlemk7u  38811  cdlemk11u  38812  cdlemk12u  38813  cdlemk26-3  38847  cdlemk37  38855  cdlemk11t  38887  cdlemk47  38890  cdlemk48  38891  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk53a  38896  cdlemk39u  38909  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord11b  39163  dihord11c  39165  dihord2pre  39166  dihord2pre2  39167  dihord5apre  39203  dihmeetlem1N  39231  dihglblem2N  39235  dihglblem3N  39236  dihglbcpreN  39241  dihmeetlem3N  39246  dihjatc1  39252  dihjatc2N  39253  dihjatc3  39254  dihmeetlem15N  39262  infleinf  42801  mullimc  43047  mullimcf  43054  limsupre  43072  addlimc  43079  limclner  43082  sge0xaddlem2  43862  itscnhlc0xyqsol  45999  itsclquadb  46010  itsclquadeu  46011