Theorem simp11l 1301

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

Assertion

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

Proof of Theorem simp11l

Step	Hyp	Ref	Expression
1		simp1l 1214	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1149	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  pceu  16896  maduf  22759  lshpsmreu  39745  exatleN  40040  2llnjaN  40202  2lplnja  40255  dalemkehl  40259  dath2  40373  pclfinN  40536  lhp2lt  40637  lhpexle3lem  40647  lhpmcvr5N  40663  lhpmcvr6N  40664  lhp2at0  40668  lhp2atnle  40669  lhp2atne  40670  lhp2at0nle  40671  lhp2at0ne  40672  4atexlemk  40683  4atexlemex6  40710  4atexlem7  40711  cdlemd2  40835  cdlemd4  40837  cdlemd7  40840  cdleme0ex2N  40860  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme11c  40897  cdleme11dN  40898  cdleme11e  40899  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15b  40911  cdleme15c  40912  cdleme15d  40913  cdleme15  40914  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme16e  40918  cdleme16f  40919  cdleme18d  40931  cdleme19b  40940  cdleme19d  40942  cdleme19e  40943  cdleme20d  40948  cdleme20e  40949  cdleme20f  40950  cdleme20g  40951  cdleme20h  40952  cdleme20j  40954  cdleme20k  40955  cdleme20l1  40956  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21c  40963  cdleme21ct  40965  cdleme21d  40966  cdleme21e  40967  cdleme22cN  40978  cdleme22f  40982  cdleme22f2  40983  cdleme22g  40984  cdleme23a  40985  cdleme23b  40986  cdleme23c  40987  cdleme25a  40989  cdleme25c  40991  cdleme25dN  40992  cdleme26ee  40996  cdleme26eALTN  40997  cdleme27a  41003  cdleme27N  41005  cdleme28a  41006  cdleme28b  41007  cdleme29ex  41010  cdlemefrs29bpre0  41032  cdlemefrs29cpre1  41034  cdlemefr29exN  41038  cdleme32fva  41073  cdleme32b  41078  cdleme32c  41079  cdleme32e  41081  cdleme35a  41084  cdleme35fnpq  41085  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35e  41089  cdleme35f  41090  cdleme36a  41096  cdleme37m  41098  cdleme39a  41101  cdleme42e  41115  cdleme42h  41118  cdleme42i  41119  cdleme42k  41120  cdleme43bN  41126  cdleme43dN  41128  cdleme17d2  41131  cdleme48bw  41138  cdlemeg46c  41149  cdlemeg46nlpq  41153  cdlemeg46ngfr  41154  cdlemeg46frv  41161  cdlemeg46vrg  41163  cdlemeg46rgv  41164  cdlemeg46req  41165  cdlemeg46gfv  41166  cdlemf1  41197  trlord  41205  cdlemb3  41242  cdlemg7fvbwN  41243  cdlemg10a  41276  cdlemg10  41277  cdlemg12e  41283  cdlemg12f  41284  cdlemg12g  41285  cdlemg12  41286  cdlemg13a  41287  cdlemg13  41288  cdlemg17b  41298  cdlemg17g  41303  cdlemg17h  41304  cdlemg17pq  41308  cdlemg17  41313  cdlemg19a  41319  cdlemg19  41320  cdlemg21  41322  cdlemg27a  41328  cdlemg27b  41332  cdlemg31c  41335  cdlemg33b0  41337  cdlemg33c0  41338  cdlemg33a  41342  cdlemg33c  41344  cdlemg33e  41346  cdlemg35  41349  trlcone  41364  tendococl  41408  cdlemh1  41451  cdlemh2  41452  cdlemh  41453  cdlemi  41456  cdlemk5  41472  cdlemk6  41473  cdlemki  41477  cdlemksv2  41483  cdlemk7  41484  cdlemk11  41485  cdlemk12  41486  cdlemkole  41489  cdlemk14  41490  cdlemk15  41491  cdlemk17  41494  cdlemk1u  41495  cdlemk5u  41497  cdlemk6u  41498  cdlemkj  41499  cdlemkuv2  41503  cdlemk7u  41506  cdlemk11u  41507  cdlemk12u  41508  cdlemk26-3  41542  cdlemk37  41550  cdlemk11t  41582  cdlemk47  41585  cdlemk48  41586  cdlemk50  41588  cdlemk51  41589  cdlemk52  41590  cdlemk53a  41591  cdlemk39u  41604  dihord1  41854  dihord2a  41855  dihord2b  41856  dihord11b  41858  dihord11c  41860  dihord2pre  41861  dihord2pre2  41862  dihord5apre  41898  dihmeetlem1N  41926  dihglblem2N  41930  dihglblem3N  41931  dihglbcpreN  41936  dihmeetlem3N  41941  dihjatc1  41947  dihjatc2N  41948  dihjatc3  41949  dihmeetlem15N  41957  infleinf  45945  mullimc  46190  mullimcf  46197  limsupre  46213  addlimc  46220  limclner  46223  sge0xaddlem2  47006  itscnhlc0xyqsol  49396  itsclquadb  49407  itsclquadeu  49408