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 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  16931  maduf  22835  lshpsmreu  39924  exatleN  40219  2llnjaN  40381  2lplnja  40434  dalemkehl  40438  dath2  40552  pclfinN  40715  lhp2lt  40816  lhpexle3lem  40826  lhpmcvr5N  40842  lhpmcvr6N  40843  lhp2at0  40847  lhp2atnle  40848  lhp2atne  40849  lhp2at0nle  40850  lhp2at0ne  40851  4atexlemk  40862  4atexlemex6  40889  4atexlem7  40890  cdlemd2  41014  cdlemd4  41016  cdlemd7  41019  cdleme0ex2N  41039  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11c  41076  cdleme11dN  41077  cdleme11e  41078  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15b  41090  cdleme15c  41091  cdleme15d  41092  cdleme15  41093  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme16f  41098  cdleme18d  41110  cdleme19b  41119  cdleme19d  41121  cdleme19e  41122  cdleme20d  41127  cdleme20e  41128  cdleme20f  41129  cdleme20g  41130  cdleme20h  41131  cdleme20j  41133  cdleme20k  41134  cdleme20l1  41135  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21c  41142  cdleme21ct  41144  cdleme21d  41145  cdleme21e  41146  cdleme22cN  41157  cdleme22f  41161  cdleme22f2  41162  cdleme22g  41163  cdleme23a  41164  cdleme23b  41165  cdleme23c  41166  cdleme25a  41168  cdleme25c  41170  cdleme25dN  41171  cdleme26ee  41175  cdleme26eALTN  41176  cdleme27a  41182  cdleme27N  41184  cdleme28a  41185  cdleme28b  41186  cdleme29ex  41189  cdlemefrs29bpre0  41211  cdlemefrs29cpre1  41213  cdlemefr29exN  41217  cdleme32fva  41252  cdleme32b  41257  cdleme32c  41258  cdleme32e  41260  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35e  41268  cdleme35f  41269  cdleme36a  41275  cdleme37m  41277  cdleme39a  41280  cdleme42e  41294  cdleme42h  41297  cdleme42i  41298  cdleme42k  41299  cdleme43bN  41305  cdleme43dN  41307  cdleme17d2  41310  cdleme48bw  41317  cdlemeg46c  41328  cdlemeg46nlpq  41332  cdlemeg46ngfr  41333  cdlemeg46frv  41340  cdlemeg46vrg  41342  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemeg46gfv  41345  cdlemf1  41376  trlord  41384  cdlemb3  41421  cdlemg7fvbwN  41422  cdlemg10a  41455  cdlemg10  41456  cdlemg12e  41462  cdlemg12f  41463  cdlemg12g  41464  cdlemg12  41465  cdlemg13a  41466  cdlemg13  41467  cdlemg17b  41477  cdlemg17g  41482  cdlemg17h  41483  cdlemg17pq  41487  cdlemg17  41492  cdlemg19a  41498  cdlemg19  41499  cdlemg21  41501  cdlemg27a  41507  cdlemg27b  41511  cdlemg31c  41514  cdlemg33b0  41516  cdlemg33c0  41517  cdlemg33a  41521  cdlemg33c  41523  cdlemg33e  41525  cdlemg35  41528  trlcone  41543  tendococl  41587  cdlemh1  41630  cdlemh2  41631  cdlemh  41632  cdlemi  41635  cdlemk5  41651  cdlemk6  41652  cdlemki  41656  cdlemksv2  41662  cdlemk7  41663  cdlemk11  41664  cdlemk12  41665  cdlemkole  41668  cdlemk14  41669  cdlemk15  41670  cdlemk17  41673  cdlemk1u  41674  cdlemk5u  41676  cdlemk6u  41677  cdlemkj  41678  cdlemkuv2  41682  cdlemk7u  41685  cdlemk11u  41686  cdlemk12u  41687  cdlemk26-3  41721  cdlemk37  41729  cdlemk11t  41761  cdlemk47  41764  cdlemk48  41765  cdlemk50  41767  cdlemk51  41768  cdlemk52  41769  cdlemk53a  41770  cdlemk39u  41783  dihord1  42033  dihord2a  42034  dihord2b  42035  dihord11b  42037  dihord11c  42039  dihord2pre  42040  dihord2pre2  42041  dihord5apre  42077  dihmeetlem1N  42105  dihglblem2N  42109  dihglblem3N  42110  dihglbcpreN  42115  dihmeetlem3N  42120  dihjatc1  42126  dihjatc2N  42127  dihjatc3  42128  dihmeetlem15N  42136  infleinf  46128  mullimc  46373  mullimcf  46380  limsupre  46396  addlimc  46403  limclner  46406  sge0xaddlem2  47189  itscnhlc0xyqsol  49586  itsclquadb  49597  itsclquadeu  49598