Theorem simp11l 1165

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  pceu  15389  maduf  20266  lshpsmreu  33414  exatleN  33708  2llnjaN  33870  2lplnja  33923  dalemkehl  33927  dath2  34041  pclfinN  34204  lhp2lt  34305  lhpexle3lem  34315  lhpmcvr5N  34331  lhpmcvr6N  34332  lhp2at0  34336  lhp2atnle  34337  lhp2atne  34338  lhp2at0nle  34339  lhp2at0ne  34340  4atexlemk  34351  4atexlemex6  34378  4atexlem7  34379  cdlemd2  34504  cdlemd4  34506  cdlemd7  34509  cdleme0ex2N  34529  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme11c  34566  cdleme11dN  34567  cdleme11e  34568  cdleme11  34575  cdleme14  34578  cdleme15a  34579  cdleme15b  34580  cdleme15c  34581  cdleme15d  34582  cdleme15  34583  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme18d  34600  cdleme19b  34610  cdleme19d  34612  cdleme19e  34613  cdleme20d  34618  cdleme20e  34619  cdleme20f  34620  cdleme20g  34621  cdleme20h  34622  cdleme20j  34624  cdleme20k  34625  cdleme20l1  34626  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme21c  34633  cdleme21ct  34635  cdleme21d  34636  cdleme21e  34637  cdleme22cN  34648  cdleme22f  34652  cdleme22f2  34653  cdleme22g  34654  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme25a  34659  cdleme25c  34661  cdleme25dN  34662  cdleme26ee  34666  cdleme26eALTN  34667  cdleme27a  34673  cdleme27N  34675  cdleme28a  34676  cdleme28b  34677  cdleme29ex  34680  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdlemefr29exN  34708  cdleme32fva  34743  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme35f  34760  cdleme36a  34766  cdleme37m  34768  cdleme39a  34771  cdleme42e  34785  cdleme42h  34788  cdleme42i  34789  cdleme42k  34790  cdleme43bN  34796  cdleme43dN  34798  cdleme17d2  34801  cdleme48bw  34808  cdlemeg46c  34819  cdlemeg46nlpq  34823  cdlemeg46ngfr  34824  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfv  34836  cdlemf1  34867  trlord  34875  cdlemb3  34912  cdlemg7fvbwN  34913  cdlemg10a  34946  cdlemg10  34947  cdlemg12e  34953  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg13  34958  cdlemg17b  34968  cdlemg17g  34973  cdlemg17h  34974  cdlemg17pq  34978  cdlemg17  34983  cdlemg19a  34989  cdlemg19  34990  cdlemg21  34992  cdlemg27a  34998  cdlemg27b  35002  cdlemg31c  35005  cdlemg33b0  35007  cdlemg33c0  35008  cdlemg33a  35012  cdlemg33c  35014  cdlemg33e  35016  cdlemg35  35019  trlcone  35034  tendococl  35078  cdlemh1  35121  cdlemh2  35122  cdlemh  35123  cdlemi  35126  cdlemk5  35142  cdlemk6  35143  cdlemki  35147  cdlemksv2  35153  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemkole  35159  cdlemk14  35160  cdlemk15  35161  cdlemk17  35164  cdlemk1u  35165  cdlemk5u  35167  cdlemk6u  35168  cdlemkj  35169  cdlemkuv2  35173  cdlemk7u  35176  cdlemk11u  35177  cdlemk12u  35178  cdlemk26-3  35212  cdlemk37  35220  cdlemk11t  35252  cdlemk47  35255  cdlemk48  35256  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  cdlemk53a  35261  cdlemk39u  35274  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord11b  35529  dihord11c  35531  dihord2pre  35532  dihord2pre2  35533  dihord5apre  35569  dihmeetlem1N  35597  dihglblem2N  35601  dihglblem3N  35602  dihglbcpreN  35607  dihmeetlem3N  35612  dihjatc1  35618  dihjatc2N  35619  dihjatc3  35620  dihmeetlem15N  35628  infleinf  38529  mullimc  38683  mullimcf  38690  limsupre  38708  addlimc  38715  limclner  38718  sge0xaddlem2  39327