Theorem simp11l 1284

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

Assertion

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

Proof of Theorem simp11l

Step	Hyp	Ref	Expression
1		simp1l 1197	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1133	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  16893  maduf  22668  lshpsmreu  39065  exatleN  39361  2llnjaN  39523  2lplnja  39576  dalemkehl  39580  dath2  39694  pclfinN  39857  lhp2lt  39958  lhpexle3lem  39968  lhpmcvr5N  39984  lhpmcvr6N  39985  lhp2at0  39989  lhp2atnle  39990  lhp2atne  39991  lhp2at0nle  39992  lhp2at0ne  39993  4atexlemk  40004  4atexlemex6  40031  4atexlem7  40032  cdlemd2  40156  cdlemd4  40158  cdlemd7  40161  cdleme0ex2N  40181  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme11c  40218  cdleme11dN  40219  cdleme11e  40220  cdleme11  40227  cdleme14  40230  cdleme15a  40231  cdleme15b  40232  cdleme15c  40233  cdleme15d  40234  cdleme15  40235  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme18d  40252  cdleme19b  40261  cdleme19d  40263  cdleme19e  40264  cdleme20d  40269  cdleme20e  40270  cdleme20f  40271  cdleme20g  40272  cdleme20h  40273  cdleme20j  40275  cdleme20k  40276  cdleme20l1  40277  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21c  40284  cdleme21ct  40286  cdleme21d  40287  cdleme21e  40288  cdleme22cN  40299  cdleme22f  40303  cdleme22f2  40304  cdleme22g  40305  cdleme23a  40306  cdleme23b  40307  cdleme23c  40308  cdleme25a  40310  cdleme25c  40312  cdleme25dN  40313  cdleme26ee  40317  cdleme26eALTN  40318  cdleme27a  40324  cdleme27N  40326  cdleme28a  40327  cdleme28b  40328  cdleme29ex  40331  cdlemefrs29bpre0  40353  cdlemefrs29cpre1  40355  cdlemefr29exN  40359  cdleme32fva  40394  cdleme32b  40399  cdleme32c  40400  cdleme32e  40402  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35e  40410  cdleme35f  40411  cdleme36a  40417  cdleme37m  40419  cdleme39a  40422  cdleme42e  40436  cdleme42h  40439  cdleme42i  40440  cdleme42k  40441  cdleme43bN  40447  cdleme43dN  40449  cdleme17d2  40452  cdleme48bw  40459  cdlemeg46c  40470  cdlemeg46nlpq  40474  cdlemeg46ngfr  40475  cdlemeg46frv  40482  cdlemeg46vrg  40484  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfv  40487  cdlemf1  40518  trlord  40526  cdlemb3  40563  cdlemg7fvbwN  40564  cdlemg10a  40597  cdlemg10  40598  cdlemg12e  40604  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg13a  40608  cdlemg13  40609  cdlemg17b  40619  cdlemg17g  40624  cdlemg17h  40625  cdlemg17pq  40629  cdlemg17  40634  cdlemg19a  40640  cdlemg19  40641  cdlemg21  40643  cdlemg27a  40649  cdlemg27b  40653  cdlemg31c  40656  cdlemg33b0  40658  cdlemg33c0  40659  cdlemg33a  40663  cdlemg33c  40665  cdlemg33e  40667  cdlemg35  40670  trlcone  40685  tendococl  40729  cdlemh1  40772  cdlemh2  40773  cdlemh  40774  cdlemi  40777  cdlemk5  40793  cdlemk6  40794  cdlemki  40798  cdlemksv2  40804  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemkole  40810  cdlemk14  40811  cdlemk15  40812  cdlemk17  40815  cdlemk1u  40816  cdlemk5u  40818  cdlemk6u  40819  cdlemkj  40820  cdlemkuv2  40824  cdlemk7u  40827  cdlemk11u  40828  cdlemk12u  40829  cdlemk26-3  40863  cdlemk37  40871  cdlemk11t  40903  cdlemk47  40906  cdlemk48  40907  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemk53a  40912  cdlemk39u  40925  dihord1  41175  dihord2a  41176  dihord2b  41177  dihord11b  41179  dihord11c  41181  dihord2pre  41182  dihord2pre2  41183  dihord5apre  41219  dihmeetlem1N  41247  dihglblem2N  41251  dihglblem3N  41252  dihglbcpreN  41257  dihmeetlem3N  41262  dihjatc1  41268  dihjatc2N  41269  dihjatc3  41270  dihmeetlem15N  41278  infleinf  45287  mullimc  45537  mullimcf  45544  limsupre  45562  addlimc  45569  limclner  45572  sge0xaddlem2  46355  itscnhlc0xyqsol  48499  itsclquadb  48510  itsclquadeu  48511