Theorem simp13l 1307

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

Assertion

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

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1220	. 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  16916  axpasch  29306  3atlem4  40292  llncvrlpln2  40363  2lplnja  40425  2lnat  40590  llnexchb2  40675  lhp2lt  40807  lhpmcvr5N  40833  4atexlemq  40857  4atexlemex6  40880  trlval2  40969  cdleme7d  41052  cdleme7e  41053  cdleme7ga  41054  cdleme7  41055  cdleme11l  41075  cdleme11  41076  cdleme14  41079  cdleme15a  41080  cdleme15b  41081  cdleme15  41084  cdleme16b  41085  cdleme16c  41086  cdleme16d  41087  cdleme18d  41101  cdleme19b  41110  cdleme19e  41113  cdleme20d  41118  cdleme20g  41121  cdleme20h  41122  cdleme20i  41123  cdleme20j  41124  cdleme20l2  41127  cdleme20l  41128  cdleme20m  41129  cdleme21d  41136  cdleme21e  41137  cdleme21h  41140  cdleme22f  41152  cdleme23a  41155  cdleme23b  41156  cdleme23c  41157  cdleme24  41158  cdleme25a  41159  cdleme25dN  41162  cdleme26ee  41166  cdleme26fALTN  41168  cdleme26f  41169  cdleme26f2ALTN  41170  cdleme26f2  41171  cdleme27a  41173  cdlemefr29bpre0N  41212  cdlemefr29clN  41213  cdlemefr32fvaN  41215  cdlemefr32fva1  41216  cdleme41sn3a  41239  cdleme35a  41254  cdleme35fnpq  41255  cdleme35b  41256  cdleme35c  41257  cdleme35d  41258  cdleme35f  41260  cdleme36m  41267  cdleme37m  41268  cdleme39n  41272  cdleme43bN  41296  cdleme43dN  41298  cdleme17d2  41301  cdlemeg46c  41319  cdlemeg46nlpq  41323  cdlemeg46ngfr  41324  cdlemeg46req  41335  cdlemeg46gfv  41336  cdleme50trn1  41355  cdleme50trn2a  41356  cdlemf1  41367  cdlemf  41369  cdlemg10a  41446  cdlemg10  41447  cdlemg12d  41452  cdlemg12e  41453  cdlemg12f  41454  cdlemg12g  41455  cdlemg12  41456  cdlemg13  41458  cdlemg16ALTN  41464  cdlemg17b  41468  cdlemg17h  41474  cdlemg17pq  41478  cdlemg17iqN  41480  cdlemg17  41483  cdlemg19a  41489  cdlemg19  41490  cdlemg21  41492  cdlemg27a  41498  cdlemg27b  41502  cdlemg31c  41505  cdlemg33b0  41507  cdlemg33a  41512  cdlemg48  41543  tendocan  41630  cdlemk26-3  41712  cdlemk27-3  41713  cdlemk28-3  41714  cdlemk37  41720  cdlemky  41732  cdlemkyu  41733  cdlemk11ta  41735  cdlemkid3N  41739  cdlemk42  41747  cdlemk42yN  41750  cdlemk11t  41752  cdlemk45  41753  cdlemk46  41754  cdlemk47  41755  cdlemk51  41759  cdlemk52  41760  cdlemk53a  41761  cdleml4N  41785  dihord2pre2  42032  dihord4  42064  dihord5apre  42068  dihmeetlem1N  42096  dihmeetlem15N  42127  mapdpglem32  42511  mzpcong  43731  mullimc  46364  mullimcf  46371  addlimc  46394  iscnrm3rlem8  49757