Theorem simp13l 1295

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

Assertion

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

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1208	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1139	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  pceu  16815  axpasch  29035  3atlem4  39985  llncvrlpln2  40056  2lplnja  40118  2lnat  40283  llnexchb2  40368  lhp2lt  40500  lhpmcvr5N  40526  4atexlemq  40550  4atexlemex6  40573  trlval2  40662  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11l  40768  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15b  40774  cdleme15  40777  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme18d  40794  cdleme19b  40803  cdleme19e  40806  cdleme20d  40811  cdleme20g  40814  cdleme20h  40815  cdleme20i  40816  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21d  40829  cdleme21e  40830  cdleme21h  40833  cdleme22f  40845  cdleme23a  40848  cdleme23b  40849  cdleme23c  40850  cdleme24  40851  cdleme25a  40852  cdleme25dN  40855  cdleme26ee  40859  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdleme27a  40866  cdlemefr29bpre0N  40905  cdlemefr29clN  40906  cdlemefr32fvaN  40908  cdlemefr32fva1  40909  cdleme41sn3a  40932  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35f  40953  cdleme36m  40960  cdleme37m  40961  cdleme39n  40965  cdleme43bN  40989  cdleme43dN  40991  cdleme17d2  40994  cdlemeg46c  41012  cdlemeg46nlpq  41016  cdlemeg46ngfr  41017  cdlemeg46req  41028  cdlemeg46gfv  41029  cdleme50trn1  41048  cdleme50trn2a  41049  cdlemf1  41060  cdlemf  41062  cdlemg10a  41139  cdlemg10  41140  cdlemg12d  41145  cdlemg12e  41146  cdlemg12f  41147  cdlemg12g  41148  cdlemg12  41149  cdlemg13  41151  cdlemg16ALTN  41157  cdlemg17b  41161  cdlemg17h  41167  cdlemg17pq  41171  cdlemg17iqN  41173  cdlemg17  41176  cdlemg19a  41182  cdlemg19  41183  cdlemg21  41185  cdlemg27a  41191  cdlemg27b  41195  cdlemg31c  41198  cdlemg33b0  41200  cdlemg33a  41205  cdlemg48  41236  tendocan  41323  cdlemk26-3  41405  cdlemk27-3  41406  cdlemk28-3  41407  cdlemk37  41413  cdlemky  41425  cdlemkyu  41426  cdlemk11ta  41428  cdlemkid3N  41432  cdlemk42  41440  cdlemk42yN  41443  cdlemk11t  41445  cdlemk45  41446  cdlemk46  41447  cdlemk47  41448  cdlemk51  41452  cdlemk52  41453  cdlemk53a  41454  cdleml4N  41478  dihord2pre2  41725  dihord4  41757  dihord5apre  41761  dihmeetlem1N  41789  dihmeetlem15N  41820  mapdpglem32  42204  mzpcong  43424  mullimc  46068  mullimcf  46075  addlimc  46098  iscnrm3rlem8  49444