Theorem simp11l 1303

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

Assertion

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

Proof of Theorem simp11l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  pceu  16907  maduf  22779  lshpsmreu  39864  exatleN  40159  2llnjaN  40321  2lplnja  40374  dalemkehl  40378  dath2  40492  pclfinN  40655  lhp2lt  40756  lhpexle3lem  40766  lhpmcvr5N  40782  lhpmcvr6N  40783  lhp2at0  40787  lhp2atnle  40788  lhp2atne  40789  lhp2at0nle  40790  lhp2at0ne  40791  4atexlemk  40802  4atexlemex6  40829  4atexlem7  40830  cdlemd2  40954  cdlemd4  40956  cdlemd7  40959  cdleme0ex2N  40979  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme11c  41016  cdleme11dN  41017  cdleme11e  41018  cdleme11  41025  cdleme14  41028  cdleme15a  41029  cdleme15b  41030  cdleme15c  41031  cdleme15d  41032  cdleme15  41033  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme18d  41050  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20d  41067  cdleme20e  41068  cdleme20f  41069  cdleme20g  41070  cdleme20h  41071  cdleme20j  41073  cdleme20k  41074  cdleme20l1  41075  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme21c  41082  cdleme21ct  41084  cdleme21d  41085  cdleme21e  41086  cdleme22cN  41097  cdleme22f  41101  cdleme22f2  41102  cdleme22g  41103  cdleme23a  41104  cdleme23b  41105  cdleme23c  41106  cdleme25a  41108  cdleme25c  41110  cdleme25dN  41111  cdleme26ee  41115  cdleme26eALTN  41116  cdleme27a  41122  cdleme27N  41124  cdleme28a  41125  cdleme28b  41126  cdleme29ex  41129  cdlemefrs29bpre0  41151  cdlemefrs29cpre1  41153  cdlemefr29exN  41157  cdleme32fva  41192  cdleme32b  41197  cdleme32c  41198  cdleme32e  41200  cdleme35a  41203  cdleme35fnpq  41204  cdleme35b  41205  cdleme35c  41206  cdleme35d  41207  cdleme35e  41208  cdleme35f  41209  cdleme36a  41215  cdleme37m  41217  cdleme39a  41220  cdleme42e  41234  cdleme42h  41237  cdleme42i  41238  cdleme42k  41239  cdleme43bN  41245  cdleme43dN  41247  cdleme17d2  41250  cdleme48bw  41257  cdlemeg46c  41268  cdlemeg46nlpq  41272  cdlemeg46ngfr  41273  cdlemeg46frv  41280  cdlemeg46vrg  41282  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemeg46gfv  41285  cdlemf1  41316  trlord  41324  cdlemb3  41361  cdlemg7fvbwN  41362  cdlemg10a  41395  cdlemg10  41396  cdlemg12e  41402  cdlemg12f  41403  cdlemg12g  41404  cdlemg12  41405  cdlemg13a  41406  cdlemg13  41407  cdlemg17b  41417  cdlemg17g  41422  cdlemg17h  41423  cdlemg17pq  41427  cdlemg17  41432  cdlemg19a  41438  cdlemg19  41439  cdlemg21  41441  cdlemg27a  41447  cdlemg27b  41451  cdlemg31c  41454  cdlemg33b0  41456  cdlemg33c0  41457  cdlemg33a  41461  cdlemg33c  41463  cdlemg33e  41465  cdlemg35  41468  trlcone  41483  tendococl  41527  cdlemh1  41570  cdlemh2  41571  cdlemh  41572  cdlemi  41575  cdlemk5  41591  cdlemk6  41592  cdlemki  41596  cdlemksv2  41602  cdlemk7  41603  cdlemk11  41604  cdlemk12  41605  cdlemkole  41608  cdlemk14  41609  cdlemk15  41610  cdlemk17  41613  cdlemk1u  41614  cdlemk5u  41616  cdlemk6u  41617  cdlemkj  41618  cdlemkuv2  41622  cdlemk7u  41625  cdlemk11u  41626  cdlemk12u  41627  cdlemk26-3  41661  cdlemk37  41669  cdlemk11t  41701  cdlemk47  41704  cdlemk48  41705  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  cdlemk53a  41710  cdlemk39u  41723  dihord1  41973  dihord2a  41974  dihord2b  41975  dihord11b  41977  dihord11c  41979  dihord2pre  41980  dihord2pre2  41981  dihord5apre  42017  dihmeetlem1N  42045  dihglblem2N  42049  dihglblem3N  42050  dihglbcpreN  42055  dihmeetlem3N  42060  dihjatc1  42066  dihjatc2N  42067  dihjatc3  42068  dihmeetlem15N  42076  infleinf  46070  mullimc  46315  mullimcf  46322  limsupre  46338  addlimc  46345  limclner  46348  sge0xaddlem2  47131  itscnhlc0xyqsol  49528  itsclquadb  49539  itsclquadeu  49540