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  17029  maduf  22961  lshpsmreu  40259  exatleN  40554  2llnjaN  40716  2lplnja  40769  dalemkehl  40773  dath2  40887  pclfinN  41050  lhp2lt  41151  lhpexle3lem  41161  lhpmcvr5N  41177  lhpmcvr6N  41178  lhp2at0  41182  lhp2atnle  41183  lhp2atne  41184  lhp2at0nle  41185  lhp2at0ne  41186  4atexlemk  41197  4atexlemex6  41224  4atexlem7  41225  cdlemd2  41349  cdlemd4  41351  cdlemd7  41354  cdleme0ex2N  41374  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme11c  41411  cdleme11dN  41412  cdleme11e  41413  cdleme11  41420  cdleme14  41423  cdleme15a  41424  cdleme15b  41425  cdleme15c  41426  cdleme15d  41427  cdleme15  41428  cdleme16b  41429  cdleme16c  41430  cdleme16d  41431  cdleme16e  41432  cdleme16f  41433  cdleme18d  41445  cdleme19b  41454  cdleme19d  41456  cdleme19e  41457  cdleme20d  41462  cdleme20e  41463  cdleme20f  41464  cdleme20g  41465  cdleme20h  41466  cdleme20j  41468  cdleme20k  41469  cdleme20l1  41470  cdleme20l2  41471  cdleme20l  41472  cdleme20m  41473  cdleme21c  41477  cdleme21ct  41479  cdleme21d  41480  cdleme21e  41481  cdleme22cN  41492  cdleme22f  41496  cdleme22f2  41497  cdleme22g  41498  cdleme23a  41499  cdleme23b  41500  cdleme23c  41501  cdleme25a  41503  cdleme25c  41505  cdleme25dN  41506  cdleme26ee  41510  cdleme26eALTN  41511  cdleme27a  41517  cdleme27N  41519  cdleme28a  41520  cdleme28b  41521  cdleme29ex  41524  cdlemefrs29bpre0  41546  cdlemefrs29cpre1  41548  cdlemefr29exN  41552  cdleme32fva  41587  cdleme32b  41592  cdleme32c  41593  cdleme32e  41595  cdleme35a  41598  cdleme35fnpq  41599  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35e  41603  cdleme35f  41604  cdleme36a  41610  cdleme37m  41612  cdleme39a  41615  cdleme42e  41629  cdleme42h  41632  cdleme42i  41633  cdleme42k  41634  cdleme43bN  41640  cdleme43dN  41642  cdleme17d2  41645  cdleme48bw  41652  cdlemeg46c  41663  cdlemeg46nlpq  41667  cdlemeg46ngfr  41668  cdlemeg46frv  41675  cdlemeg46vrg  41677  cdlemeg46rgv  41678  cdlemeg46req  41679  cdlemeg46gfv  41680  cdlemf1  41711  trlord  41719  cdlemb3  41756  cdlemg7fvbwN  41757  cdlemg10a  41790  cdlemg10  41791  cdlemg12e  41797  cdlemg12f  41798  cdlemg12g  41799  cdlemg12  41800  cdlemg13a  41801  cdlemg13  41802  cdlemg17b  41812  cdlemg17g  41817  cdlemg17h  41818  cdlemg17pq  41822  cdlemg17  41827  cdlemg19a  41833  cdlemg19  41834  cdlemg21  41836  cdlemg27a  41842  cdlemg27b  41846  cdlemg31c  41849  cdlemg33b0  41851  cdlemg33c0  41852  cdlemg33a  41856  cdlemg33c  41858  cdlemg33e  41860  cdlemg35  41863  trlcone  41878  tendococl  41922  cdlemh1  41965  cdlemh2  41966  cdlemh  41967  cdlemi  41970  cdlemk5  41986  cdlemk6  41987  cdlemki  41991  cdlemksv2  41997  cdlemk7  41998  cdlemk11  41999  cdlemk12  42000  cdlemkole  42003  cdlemk14  42004  cdlemk15  42005  cdlemk17  42008  cdlemk1u  42009  cdlemk5u  42011  cdlemk6u  42012  cdlemkj  42013  cdlemkuv2  42017  cdlemk7u  42020  cdlemk11u  42021  cdlemk12u  42022  cdlemk26-3  42056  cdlemk37  42064  cdlemk11t  42096  cdlemk47  42099  cdlemk48  42100  cdlemk50  42102  cdlemk51  42103  cdlemk52  42104  cdlemk53a  42105  cdlemk39u  42118  dihord1  42368  dihord2a  42369  dihord2b  42370  dihord11b  42372  dihord11c  42374  dihord2pre  42375  dihord2pre2  42376  dihord5apre  42412  dihmeetlem1N  42440  dihglblem2N  42444  dihglblem3N  42445  dihglbcpreN  42450  dihmeetlem3N  42455  dihjatc1  42461  dihjatc2N  42462  dihjatc3  42463  dihmeetlem15N  42471  infleinf  46476  mullimc  46721  mullimcf  46728  limsupre  46744  addlimc  46751  limclner  46754  sge0xaddlem2  47537  itscnhlc0xyqsol  49970  itsclquadb  49981  itsclquadeu  49982