Theorem simp11l 1283

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

Assertion

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

Proof of Theorem simp11l

Step	Hyp	Ref	Expression
1		simp1l 1196	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1132	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  16879  maduf  22662  lshpsmreu  39090  exatleN  39386  2llnjaN  39548  2lplnja  39601  dalemkehl  39605  dath2  39719  pclfinN  39882  lhp2lt  39983  lhpexle3lem  39993  lhpmcvr5N  40009  lhpmcvr6N  40010  lhp2at0  40014  lhp2atnle  40015  lhp2atne  40016  lhp2at0nle  40017  lhp2at0ne  40018  4atexlemk  40029  4atexlemex6  40056  4atexlem7  40057  cdlemd2  40181  cdlemd4  40183  cdlemd7  40186  cdleme0ex2N  40206  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme11c  40243  cdleme11dN  40244  cdleme11e  40245  cdleme11  40252  cdleme14  40255  cdleme15a  40256  cdleme15b  40257  cdleme15c  40258  cdleme15d  40259  cdleme15  40260  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme18d  40277  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20d  40294  cdleme20e  40295  cdleme20f  40296  cdleme20g  40297  cdleme20h  40298  cdleme20j  40300  cdleme20k  40301  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21c  40309  cdleme21ct  40311  cdleme21d  40312  cdleme21e  40313  cdleme22cN  40324  cdleme22f  40328  cdleme22f2  40329  cdleme22g  40330  cdleme23a  40331  cdleme23b  40332  cdleme23c  40333  cdleme25a  40335  cdleme25c  40337  cdleme25dN  40338  cdleme26ee  40342  cdleme26eALTN  40343  cdleme27a  40349  cdleme27N  40351  cdleme28a  40352  cdleme28b  40353  cdleme29ex  40356  cdlemefrs29bpre0  40378  cdlemefrs29cpre1  40380  cdlemefr29exN  40384  cdleme32fva  40419  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35a  40430  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35e  40435  cdleme35f  40436  cdleme36a  40442  cdleme37m  40444  cdleme39a  40447  cdleme42e  40461  cdleme42h  40464  cdleme42i  40465  cdleme42k  40466  cdleme43bN  40472  cdleme43dN  40474  cdleme17d2  40477  cdleme48bw  40484  cdlemeg46c  40495  cdlemeg46nlpq  40499  cdlemeg46ngfr  40500  cdlemeg46frv  40507  cdlemeg46vrg  40509  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdlemf1  40543  trlord  40551  cdlemb3  40588  cdlemg7fvbwN  40589  cdlemg10a  40622  cdlemg10  40623  cdlemg12e  40629  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg13  40634  cdlemg17b  40644  cdlemg17g  40649  cdlemg17h  40650  cdlemg17pq  40654  cdlemg17  40659  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg27b  40678  cdlemg31c  40681  cdlemg33b0  40683  cdlemg33c0  40684  cdlemg33a  40688  cdlemg33c  40690  cdlemg33e  40692  cdlemg35  40695  trlcone  40710  tendococl  40754  cdlemh1  40797  cdlemh2  40798  cdlemh  40799  cdlemi  40802  cdlemk5  40818  cdlemk6  40819  cdlemki  40823  cdlemksv2  40829  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemkole  40835  cdlemk14  40836  cdlemk15  40837  cdlemk17  40840  cdlemk1u  40841  cdlemk5u  40843  cdlemk6u  40844  cdlemkj  40845  cdlemkuv2  40849  cdlemk7u  40852  cdlemk11u  40853  cdlemk12u  40854  cdlemk26-3  40888  cdlemk37  40896  cdlemk11t  40928  cdlemk47  40931  cdlemk48  40932  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  cdlemk53a  40937  cdlemk39u  40950  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord11b  41204  dihord11c  41206  dihord2pre  41207  dihord2pre2  41208  dihord5apre  41244  dihmeetlem1N  41272  dihglblem2N  41276  dihglblem3N  41277  dihglbcpreN  41282  dihmeetlem3N  41287  dihjatc1  41293  dihjatc2N  41294  dihjatc3  41295  dihmeetlem15N  41303  infleinf  45321  mullimc  45571  mullimcf  45578  limsupre  45596  addlimc  45603  limclner  45606  sge0xaddlem2  46389  itscnhlc0xyqsol  48614  itsclquadb  48625  itsclquadeu  48626