Theorem simp11l 1286

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

Assertion

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

Proof of Theorem simp11l

Step	Hyp	Ref	Expression
1		simp1l 1199	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1134	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  16817  maduf  22606  lshpsmreu  39555  exatleN  39850  2llnjaN  40012  2lplnja  40065  dalemkehl  40069  dath2  40183  pclfinN  40346  lhp2lt  40447  lhpexle3lem  40457  lhpmcvr5N  40473  lhpmcvr6N  40474  lhp2at0  40478  lhp2atnle  40479  lhp2atne  40480  lhp2at0nle  40481  lhp2at0ne  40482  4atexlemk  40493  4atexlemex6  40520  4atexlem7  40521  cdlemd2  40645  cdlemd4  40647  cdlemd7  40650  cdleme0ex2N  40670  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme11c  40707  cdleme11dN  40708  cdleme11e  40709  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme15b  40721  cdleme15c  40722  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme18d  40741  cdleme19b  40750  cdleme19d  40752  cdleme19e  40753  cdleme20d  40758  cdleme20e  40759  cdleme20f  40760  cdleme20g  40761  cdleme20h  40762  cdleme20j  40764  cdleme20k  40765  cdleme20l1  40766  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21c  40773  cdleme21ct  40775  cdleme21d  40776  cdleme21e  40777  cdleme22cN  40788  cdleme22f  40792  cdleme22f2  40793  cdleme22g  40794  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme25a  40799  cdleme25c  40801  cdleme25dN  40802  cdleme26ee  40806  cdleme26eALTN  40807  cdleme27a  40813  cdleme27N  40815  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdlemefr29exN  40848  cdleme32fva  40883  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme36a  40906  cdleme37m  40908  cdleme39a  40911  cdleme42e  40925  cdleme42h  40928  cdleme42i  40929  cdleme42k  40930  cdleme43bN  40936  cdleme43dN  40938  cdleme17d2  40941  cdleme48bw  40948  cdlemeg46c  40959  cdlemeg46nlpq  40963  cdlemeg46ngfr  40964  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemeg46gfv  40976  cdlemf1  41007  trlord  41015  cdlemb3  41052  cdlemg7fvbwN  41053  cdlemg10a  41086  cdlemg10  41087  cdlemg12e  41093  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg13  41098  cdlemg17b  41108  cdlemg17g  41113  cdlemg17h  41114  cdlemg17pq  41118  cdlemg17  41123  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg27b  41142  cdlemg31c  41145  cdlemg33b0  41147  cdlemg33c0  41148  cdlemg33a  41152  cdlemg33c  41154  cdlemg33e  41156  cdlemg35  41159  trlcone  41174  tendococl  41218  cdlemh1  41261  cdlemh2  41262  cdlemh  41263  cdlemi  41266  cdlemk5  41282  cdlemk6  41283  cdlemki  41287  cdlemksv2  41293  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk17  41304  cdlemk1u  41305  cdlemk5u  41307  cdlemk6u  41308  cdlemkj  41309  cdlemkuv2  41313  cdlemk7u  41316  cdlemk11u  41317  cdlemk12u  41318  cdlemk26-3  41352  cdlemk37  41360  cdlemk11t  41392  cdlemk47  41395  cdlemk48  41396  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  cdlemk53a  41401  cdlemk39u  41414  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord11b  41668  dihord11c  41670  dihord2pre  41671  dihord2pre2  41672  dihord5apre  41708  dihmeetlem1N  41736  dihglblem2N  41740  dihglblem3N  41741  dihglbcpreN  41746  dihmeetlem3N  41751  dihjatc1  41757  dihjatc2N  41758  dihjatc3  41759  dihmeetlem15N  41767  infleinf  45801  mullimc  46046  mullimcf  46053  limsupre  46069  addlimc  46076  limclner  46079  sge0xaddlem2  46862  itscnhlc0xyqsol  49241  itsclquadb  49252  itsclquadeu  49253