Theorem simp11l 1297

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  pceu  16865  maduf  22681  lshpsmreu  39697  exatleN  39992  2llnjaN  40154  2lplnja  40207  dalemkehl  40211  dath2  40325  pclfinN  40488  lhp2lt  40589  lhpexle3lem  40599  lhpmcvr5N  40615  lhpmcvr6N  40616  lhp2at0  40620  lhp2atnle  40621  lhp2atne  40622  lhp2at0nle  40623  lhp2at0ne  40624  4atexlemk  40635  4atexlemex6  40662  4atexlem7  40663  cdlemd2  40787  cdlemd4  40789  cdlemd7  40792  cdleme0ex2N  40812  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme11c  40849  cdleme11dN  40850  cdleme11e  40851  cdleme11  40858  cdleme14  40861  cdleme15a  40862  cdleme15b  40863  cdleme15c  40864  cdleme15d  40865  cdleme15  40866  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme16e  40870  cdleme16f  40871  cdleme18d  40883  cdleme19b  40892  cdleme19d  40894  cdleme19e  40895  cdleme20d  40900  cdleme20e  40901  cdleme20f  40902  cdleme20g  40903  cdleme20h  40904  cdleme20j  40906  cdleme20k  40907  cdleme20l1  40908  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme21c  40915  cdleme21ct  40917  cdleme21d  40918  cdleme21e  40919  cdleme22cN  40930  cdleme22f  40934  cdleme22f2  40935  cdleme22g  40936  cdleme23a  40937  cdleme23b  40938  cdleme23c  40939  cdleme25a  40941  cdleme25c  40943  cdleme25dN  40944  cdleme26ee  40948  cdleme26eALTN  40949  cdleme27a  40955  cdleme27N  40957  cdleme28a  40958  cdleme28b  40959  cdleme29ex  40962  cdlemefrs29bpre0  40984  cdlemefrs29cpre1  40986  cdlemefr29exN  40990  cdleme32fva  41025  cdleme32b  41030  cdleme32c  41031  cdleme32e  41033  cdleme35a  41036  cdleme35fnpq  41037  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35e  41041  cdleme35f  41042  cdleme36a  41048  cdleme37m  41050  cdleme39a  41053  cdleme42e  41067  cdleme42h  41070  cdleme42i  41071  cdleme42k  41072  cdleme43bN  41078  cdleme43dN  41080  cdleme17d2  41083  cdleme48bw  41090  cdlemeg46c  41101  cdlemeg46nlpq  41105  cdlemeg46ngfr  41106  cdlemeg46frv  41113  cdlemeg46vrg  41115  cdlemeg46rgv  41116  cdlemeg46req  41117  cdlemeg46gfv  41118  cdlemf1  41149  trlord  41157  cdlemb3  41194  cdlemg7fvbwN  41195  cdlemg10a  41228  cdlemg10  41229  cdlemg12e  41235  cdlemg12f  41236  cdlemg12g  41237  cdlemg12  41238  cdlemg13a  41239  cdlemg13  41240  cdlemg17b  41250  cdlemg17g  41255  cdlemg17h  41256  cdlemg17pq  41260  cdlemg17  41265  cdlemg19a  41271  cdlemg19  41272  cdlemg21  41274  cdlemg27a  41280  cdlemg27b  41284  cdlemg31c  41287  cdlemg33b0  41289  cdlemg33c0  41290  cdlemg33a  41294  cdlemg33c  41296  cdlemg33e  41298  cdlemg35  41301  trlcone  41316  tendococl  41360  cdlemh1  41403  cdlemh2  41404  cdlemh  41405  cdlemi  41408  cdlemk5  41424  cdlemk6  41425  cdlemki  41429  cdlemksv2  41435  cdlemk7  41436  cdlemk11  41437  cdlemk12  41438  cdlemkole  41441  cdlemk14  41442  cdlemk15  41443  cdlemk17  41446  cdlemk1u  41447  cdlemk5u  41449  cdlemk6u  41450  cdlemkj  41451  cdlemkuv2  41455  cdlemk7u  41458  cdlemk11u  41459  cdlemk12u  41460  cdlemk26-3  41494  cdlemk37  41502  cdlemk11t  41534  cdlemk47  41537  cdlemk48  41538  cdlemk50  41540  cdlemk51  41541  cdlemk52  41542  cdlemk53a  41543  cdlemk39u  41556  dihord1  41806  dihord2a  41807  dihord2b  41808  dihord11b  41810  dihord11c  41812  dihord2pre  41813  dihord2pre2  41814  dihord5apre  41850  dihmeetlem1N  41878  dihglblem2N  41882  dihglblem3N  41883  dihglbcpreN  41888  dihmeetlem3N  41893  dihjatc1  41899  dihjatc2N  41900  dihjatc3  41901  dihmeetlem15N  41909  infleinf  45911  mullimc  46156  mullimcf  46163  limsupre  46179  addlimc  46186  limclner  46189  sge0xaddlem2  46972  itscnhlc0xyqsol  49351  itsclquadb  49362  itsclquadeu  49363