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  17004  maduf  22936  lshpsmreu  40134  exatleN  40429  2llnjaN  40591  2lplnja  40644  dalemkehl  40648  dath2  40762  pclfinN  40925  lhp2lt  41026  lhpexle3lem  41036  lhpmcvr5N  41052  lhpmcvr6N  41053  lhp2at0  41057  lhp2atnle  41058  lhp2atne  41059  lhp2at0nle  41060  lhp2at0ne  41061  4atexlemk  41072  4atexlemex6  41099  4atexlem7  41100  cdlemd2  41224  cdlemd4  41226  cdlemd7  41229  cdleme0ex2N  41249  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11c  41286  cdleme11dN  41287  cdleme11e  41288  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15b  41300  cdleme15c  41301  cdleme15d  41302  cdleme15  41303  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme16f  41308  cdleme18d  41320  cdleme19b  41329  cdleme19d  41331  cdleme19e  41332  cdleme20d  41337  cdleme20e  41338  cdleme20f  41339  cdleme20g  41340  cdleme20h  41341  cdleme20j  41343  cdleme20k  41344  cdleme20l1  41345  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21c  41352  cdleme21ct  41354  cdleme21d  41355  cdleme21e  41356  cdleme22cN  41367  cdleme22f  41371  cdleme22f2  41372  cdleme22g  41373  cdleme23a  41374  cdleme23b  41375  cdleme23c  41376  cdleme25a  41378  cdleme25c  41380  cdleme25dN  41381  cdleme26ee  41385  cdleme26eALTN  41386  cdleme27a  41392  cdleme27N  41394  cdleme28a  41395  cdleme28b  41396  cdleme29ex  41399  cdlemefrs29bpre0  41421  cdlemefrs29cpre1  41423  cdlemefr29exN  41427  cdleme32fva  41462  cdleme32b  41467  cdleme32c  41468  cdleme32e  41470  cdleme35a  41473  cdleme35fnpq  41474  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35e  41478  cdleme35f  41479  cdleme36a  41485  cdleme37m  41487  cdleme39a  41490  cdleme42e  41504  cdleme42h  41507  cdleme42i  41508  cdleme42k  41509  cdleme43bN  41515  cdleme43dN  41517  cdleme17d2  41520  cdleme48bw  41527  cdlemeg46c  41538  cdlemeg46nlpq  41542  cdlemeg46ngfr  41543  cdlemeg46frv  41550  cdlemeg46vrg  41552  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemeg46gfv  41555  cdlemf1  41586  trlord  41594  cdlemb3  41631  cdlemg7fvbwN  41632  cdlemg10a  41665  cdlemg10  41666  cdlemg12e  41672  cdlemg12f  41673  cdlemg12g  41674  cdlemg12  41675  cdlemg13a  41676  cdlemg13  41677  cdlemg17b  41687  cdlemg17g  41692  cdlemg17h  41693  cdlemg17pq  41697  cdlemg17  41702  cdlemg19a  41708  cdlemg19  41709  cdlemg21  41711  cdlemg27a  41717  cdlemg27b  41721  cdlemg31c  41724  cdlemg33b0  41726  cdlemg33c0  41727  cdlemg33a  41731  cdlemg33c  41733  cdlemg33e  41735  cdlemg35  41738  trlcone  41753  tendococl  41797  cdlemh1  41840  cdlemh2  41841  cdlemh  41842  cdlemi  41845  cdlemk5  41861  cdlemk6  41862  cdlemki  41866  cdlemksv2  41872  cdlemk7  41873  cdlemk11  41874  cdlemk12  41875  cdlemkole  41878  cdlemk14  41879  cdlemk15  41880  cdlemk17  41883  cdlemk1u  41884  cdlemk5u  41886  cdlemk6u  41887  cdlemkj  41888  cdlemkuv2  41892  cdlemk7u  41895  cdlemk11u  41896  cdlemk12u  41897  cdlemk26-3  41931  cdlemk37  41939  cdlemk11t  41971  cdlemk47  41974  cdlemk48  41975  cdlemk50  41977  cdlemk51  41978  cdlemk52  41979  cdlemk53a  41980  cdlemk39u  41993  dihord1  42243  dihord2a  42244  dihord2b  42245  dihord11b  42247  dihord11c  42249  dihord2pre  42250  dihord2pre2  42251  dihord5apre  42287  dihmeetlem1N  42315  dihglblem2N  42319  dihglblem3N  42320  dihglbcpreN  42325  dihmeetlem3N  42330  dihjatc1  42336  dihjatc2N  42337  dihjatc3  42338  dihmeetlem15N  42346  infleinf  46327  mullimc  46572  mullimcf  46579  limsupre  46595  addlimc  46602  limclner  46605  sge0xaddlem2  47388  itscnhlc0xyqsol  49821  itsclquadb  49832  itsclquadeu  49833