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

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

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 1088

This theorem is referenced by:  pceu  16755  maduf  22554  lshpsmreu  39147  exatleN  39442  2llnjaN  39604  2lplnja  39657  dalemkehl  39661  dath2  39775  pclfinN  39938  lhp2lt  40039  lhpexle3lem  40049  lhpmcvr5N  40065  lhpmcvr6N  40066  lhp2at0  40070  lhp2atnle  40071  lhp2atne  40072  lhp2at0nle  40073  lhp2at0ne  40074  4atexlemk  40085  4atexlemex6  40112  4atexlem7  40113  cdlemd2  40237  cdlemd4  40239  cdlemd7  40242  cdleme0ex2N  40262  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme11c  40299  cdleme11dN  40300  cdleme11e  40301  cdleme11  40308  cdleme14  40311  cdleme15a  40312  cdleme15b  40313  cdleme15c  40314  cdleme15d  40315  cdleme15  40316  cdleme16b  40317  cdleme16c  40318  cdleme16d  40319  cdleme16e  40320  cdleme16f  40321  cdleme18d  40333  cdleme19b  40342  cdleme19d  40344  cdleme19e  40345  cdleme20d  40350  cdleme20e  40351  cdleme20f  40352  cdleme20g  40353  cdleme20h  40354  cdleme20j  40356  cdleme20k  40357  cdleme20l1  40358  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21c  40365  cdleme21ct  40367  cdleme21d  40368  cdleme21e  40369  cdleme22cN  40380  cdleme22f  40384  cdleme22f2  40385  cdleme22g  40386  cdleme23a  40387  cdleme23b  40388  cdleme23c  40389  cdleme25a  40391  cdleme25c  40393  cdleme25dN  40394  cdleme26ee  40398  cdleme26eALTN  40399  cdleme27a  40405  cdleme27N  40407  cdleme28a  40408  cdleme28b  40409  cdleme29ex  40412  cdlemefrs29bpre0  40434  cdlemefrs29cpre1  40436  cdlemefr29exN  40440  cdleme32fva  40475  cdleme32b  40480  cdleme32c  40481  cdleme32e  40483  cdleme35a  40486  cdleme35fnpq  40487  cdleme35b  40488  cdleme35c  40489  cdleme35d  40490  cdleme35e  40491  cdleme35f  40492  cdleme36a  40498  cdleme37m  40500  cdleme39a  40503  cdleme42e  40517  cdleme42h  40520  cdleme42i  40521  cdleme42k  40522  cdleme43bN  40528  cdleme43dN  40530  cdleme17d2  40533  cdleme48bw  40540  cdlemeg46c  40551  cdlemeg46nlpq  40555  cdlemeg46ngfr  40556  cdlemeg46frv  40563  cdlemeg46vrg  40565  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemeg46gfv  40568  cdlemf1  40599  trlord  40607  cdlemb3  40644  cdlemg7fvbwN  40645  cdlemg10a  40678  cdlemg10  40679  cdlemg12e  40685  cdlemg12f  40686  cdlemg12g  40687  cdlemg12  40688  cdlemg13a  40689  cdlemg13  40690  cdlemg17b  40700  cdlemg17g  40705  cdlemg17h  40706  cdlemg17pq  40710  cdlemg17  40715  cdlemg19a  40721  cdlemg19  40722  cdlemg21  40724  cdlemg27a  40730  cdlemg27b  40734  cdlemg31c  40737  cdlemg33b0  40739  cdlemg33c0  40740  cdlemg33a  40744  cdlemg33c  40746  cdlemg33e  40748  cdlemg35  40751  trlcone  40766  tendococl  40810  cdlemh1  40853  cdlemh2  40854  cdlemh  40855  cdlemi  40858  cdlemk5  40874  cdlemk6  40875  cdlemki  40879  cdlemksv2  40885  cdlemk7  40886  cdlemk11  40887  cdlemk12  40888  cdlemkole  40891  cdlemk14  40892  cdlemk15  40893  cdlemk17  40896  cdlemk1u  40897  cdlemk5u  40899  cdlemk6u  40900  cdlemkj  40901  cdlemkuv2  40905  cdlemk7u  40908  cdlemk11u  40909  cdlemk12u  40910  cdlemk26-3  40944  cdlemk37  40952  cdlemk11t  40984  cdlemk47  40987  cdlemk48  40988  cdlemk50  40990  cdlemk51  40991  cdlemk52  40992  cdlemk53a  40993  cdlemk39u  41006  dihord1  41256  dihord2a  41257  dihord2b  41258  dihord11b  41260  dihord11c  41262  dihord2pre  41263  dihord2pre2  41264  dihord5apre  41300  dihmeetlem1N  41328  dihglblem2N  41332  dihglblem3N  41333  dihglbcpreN  41338  dihmeetlem3N  41343  dihjatc1  41349  dihjatc2N  41350  dihjatc3  41351  dihmeetlem15N  41359  infleinf  45409  mullimc  45655  mullimcf  45662  limsupre  45678  addlimc  45685  limclner  45688  sge0xaddlem2  46471  itscnhlc0xyqsol  48796  itsclquadb  48807  itsclquadeu  48808