Theorem simp11l 1281

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  pceu  16843  maduf  22626  lshpsmreu  38755  exatleN  39051  2llnjaN  39213  2lplnja  39266  dalemkehl  39270  dath2  39384  pclfinN  39547  lhp2lt  39648  lhpexle3lem  39658  lhpmcvr5N  39674  lhpmcvr6N  39675  lhp2at0  39679  lhp2atnle  39680  lhp2atne  39681  lhp2at0nle  39682  lhp2at0ne  39683  4atexlemk  39694  4atexlemex6  39721  4atexlem7  39722  cdlemd2  39846  cdlemd4  39848  cdlemd7  39851  cdleme0ex2N  39871  cdleme7aa  39889  cdleme7c  39892  cdleme7d  39893  cdleme7e  39894  cdleme7ga  39895  cdleme7  39896  cdleme11c  39908  cdleme11dN  39909  cdleme11e  39910  cdleme11  39917  cdleme14  39920  cdleme15a  39921  cdleme15b  39922  cdleme15c  39923  cdleme15d  39924  cdleme15  39925  cdleme16b  39926  cdleme16c  39927  cdleme16d  39928  cdleme16e  39929  cdleme16f  39930  cdleme18d  39942  cdleme19b  39951  cdleme19d  39953  cdleme19e  39954  cdleme20d  39959  cdleme20e  39960  cdleme20f  39961  cdleme20g  39962  cdleme20h  39963  cdleme20j  39965  cdleme20k  39966  cdleme20l1  39967  cdleme20l2  39968  cdleme20l  39969  cdleme20m  39970  cdleme21c  39974  cdleme21ct  39976  cdleme21d  39977  cdleme21e  39978  cdleme22cN  39989  cdleme22f  39993  cdleme22f2  39994  cdleme22g  39995  cdleme23a  39996  cdleme23b  39997  cdleme23c  39998  cdleme25a  40000  cdleme25c  40002  cdleme25dN  40003  cdleme26ee  40007  cdleme26eALTN  40008  cdleme27a  40014  cdleme27N  40016  cdleme28a  40017  cdleme28b  40018  cdleme29ex  40021  cdlemefrs29bpre0  40043  cdlemefrs29cpre1  40045  cdlemefr29exN  40049  cdleme32fva  40084  cdleme32b  40089  cdleme32c  40090  cdleme32e  40092  cdleme35a  40095  cdleme35fnpq  40096  cdleme35b  40097  cdleme35c  40098  cdleme35d  40099  cdleme35e  40100  cdleme35f  40101  cdleme36a  40107  cdleme37m  40109  cdleme39a  40112  cdleme42e  40126  cdleme42h  40129  cdleme42i  40130  cdleme42k  40131  cdleme43bN  40137  cdleme43dN  40139  cdleme17d2  40142  cdleme48bw  40149  cdlemeg46c  40160  cdlemeg46nlpq  40164  cdlemeg46ngfr  40165  cdlemeg46frv  40172  cdlemeg46vrg  40174  cdlemeg46rgv  40175  cdlemeg46req  40176  cdlemeg46gfv  40177  cdlemf1  40208  trlord  40216  cdlemb3  40253  cdlemg7fvbwN  40254  cdlemg10a  40287  cdlemg10  40288  cdlemg12e  40294  cdlemg12f  40295  cdlemg12g  40296  cdlemg12  40297  cdlemg13a  40298  cdlemg13  40299  cdlemg17b  40309  cdlemg17g  40314  cdlemg17h  40315  cdlemg17pq  40319  cdlemg17  40324  cdlemg19a  40330  cdlemg19  40331  cdlemg21  40333  cdlemg27a  40339  cdlemg27b  40343  cdlemg31c  40346  cdlemg33b0  40348  cdlemg33c0  40349  cdlemg33a  40353  cdlemg33c  40355  cdlemg33e  40357  cdlemg35  40360  trlcone  40375  tendococl  40419  cdlemh1  40462  cdlemh2  40463  cdlemh  40464  cdlemi  40467  cdlemk5  40483  cdlemk6  40484  cdlemki  40488  cdlemksv2  40494  cdlemk7  40495  cdlemk11  40496  cdlemk12  40497  cdlemkole  40500  cdlemk14  40501  cdlemk15  40502  cdlemk17  40505  cdlemk1u  40506  cdlemk5u  40508  cdlemk6u  40509  cdlemkj  40510  cdlemkuv2  40514  cdlemk7u  40517  cdlemk11u  40518  cdlemk12u  40519  cdlemk26-3  40553  cdlemk37  40561  cdlemk11t  40593  cdlemk47  40596  cdlemk48  40597  cdlemk50  40599  cdlemk51  40600  cdlemk52  40601  cdlemk53a  40602  cdlemk39u  40615  dihord1  40865  dihord2a  40866  dihord2b  40867  dihord11b  40869  dihord11c  40871  dihord2pre  40872  dihord2pre2  40873  dihord5apre  40909  dihmeetlem1N  40937  dihglblem2N  40941  dihglblem3N  40942  dihglbcpreN  40947  dihmeetlem3N  40952  dihjatc1  40958  dihjatc2N  40959  dihjatc3  40960  dihmeetlem15N  40968  infleinf  44924  mullimc  45174  mullimcf  45181  limsupre  45199  addlimc  45206  limclner  45209  sge0xaddlem2  45992  itscnhlc0xyqsol  48090  itsclquadb  48101  itsclquadeu  48102