Theorem simp11l 1285

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

Assertion

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

Proof of Theorem simp11l

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  pceu  16884  maduf  22647  lshpsmreu  39110  exatleN  39406  2llnjaN  39568  2lplnja  39621  dalemkehl  39625  dath2  39739  pclfinN  39902  lhp2lt  40003  lhpexle3lem  40013  lhpmcvr5N  40029  lhpmcvr6N  40030  lhp2at0  40034  lhp2atnle  40035  lhp2atne  40036  lhp2at0nle  40037  lhp2at0ne  40038  4atexlemk  40049  4atexlemex6  40076  4atexlem7  40077  cdlemd2  40201  cdlemd4  40203  cdlemd7  40206  cdleme0ex2N  40226  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme11c  40263  cdleme11dN  40264  cdleme11e  40265  cdleme11  40272  cdleme14  40275  cdleme15a  40276  cdleme15b  40277  cdleme15c  40278  cdleme15d  40279  cdleme15  40280  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme18d  40297  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20d  40314  cdleme20e  40315  cdleme20f  40316  cdleme20g  40317  cdleme20h  40318  cdleme20j  40320  cdleme20k  40321  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21c  40329  cdleme21ct  40331  cdleme21d  40332  cdleme21e  40333  cdleme22cN  40344  cdleme22f  40348  cdleme22f2  40349  cdleme22g  40350  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme25a  40355  cdleme25c  40357  cdleme25dN  40358  cdleme26ee  40362  cdleme26eALTN  40363  cdleme27a  40369  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdlemefr29exN  40404  cdleme32fva  40439  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35a  40450  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme35f  40456  cdleme36a  40462  cdleme37m  40464  cdleme39a  40467  cdleme42e  40481  cdleme42h  40484  cdleme42i  40485  cdleme42k  40486  cdleme43bN  40492  cdleme43dN  40494  cdleme17d2  40497  cdleme48bw  40504  cdlemeg46c  40515  cdlemeg46nlpq  40519  cdlemeg46ngfr  40520  cdlemeg46frv  40527  cdlemeg46vrg  40529  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfv  40532  cdlemf1  40563  trlord  40571  cdlemb3  40608  cdlemg7fvbwN  40609  cdlemg10a  40642  cdlemg10  40643  cdlemg12e  40649  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg13  40654  cdlemg17b  40664  cdlemg17g  40669  cdlemg17h  40670  cdlemg17pq  40674  cdlemg17  40679  cdlemg19a  40685  cdlemg19  40686  cdlemg21  40688  cdlemg27a  40694  cdlemg27b  40698  cdlemg31c  40701  cdlemg33b0  40703  cdlemg33c0  40704  cdlemg33a  40708  cdlemg33c  40710  cdlemg33e  40712  cdlemg35  40715  trlcone  40730  tendococl  40774  cdlemh1  40817  cdlemh2  40818  cdlemh  40819  cdlemi  40822  cdlemk5  40838  cdlemk6  40839  cdlemki  40843  cdlemksv2  40849  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemkole  40855  cdlemk14  40856  cdlemk15  40857  cdlemk17  40860  cdlemk1u  40861  cdlemk5u  40863  cdlemk6u  40864  cdlemkj  40865  cdlemkuv2  40869  cdlemk7u  40872  cdlemk11u  40873  cdlemk12u  40874  cdlemk26-3  40908  cdlemk37  40916  cdlemk11t  40948  cdlemk47  40951  cdlemk48  40952  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk53a  40957  cdlemk39u  40970  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihord2pre2  41228  dihord5apre  41264  dihmeetlem1N  41292  dihglblem2N  41296  dihglblem3N  41297  dihglbcpreN  41302  dihmeetlem3N  41307  dihjatc1  41313  dihjatc2N  41314  dihjatc3  41315  dihmeetlem15N  41323  infleinf  45383  mullimc  45631  mullimcf  45638  limsupre  45656  addlimc  45663  limclner  45666  sge0xaddlem2  46449  itscnhlc0xyqsol  48686  itsclquadb  48697  itsclquadeu  48698