Theorem simp13l 1289

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

Assertion

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

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1202	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1133	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  16774  axpasch  29014  3atlem4  39742  llncvrlpln2  39813  2lplnja  39875  2lnat  40040  llnexchb2  40125  lhp2lt  40257  lhpmcvr5N  40283  4atexlemq  40307  4atexlemex6  40330  trlval2  40419  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11l  40525  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15b  40531  cdleme15  40534  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme18d  40551  cdleme19b  40560  cdleme19e  40563  cdleme20d  40568  cdleme20g  40571  cdleme20h  40572  cdleme20i  40573  cdleme20j  40574  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21d  40586  cdleme21e  40587  cdleme21h  40590  cdleme22f  40602  cdleme23a  40605  cdleme23b  40606  cdleme23c  40607  cdleme24  40608  cdleme25a  40609  cdleme25dN  40612  cdleme26ee  40616  cdleme26fALTN  40618  cdleme26f  40619  cdleme26f2ALTN  40620  cdleme26f2  40621  cdleme27a  40623  cdlemefr29bpre0N  40662  cdlemefr29clN  40663  cdlemefr32fvaN  40665  cdlemefr32fva1  40666  cdleme41sn3a  40689  cdleme35a  40704  cdleme35fnpq  40705  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35f  40710  cdleme36m  40717  cdleme37m  40718  cdleme39n  40722  cdleme43bN  40746  cdleme43dN  40748  cdleme17d2  40751  cdlemeg46c  40769  cdlemeg46nlpq  40773  cdlemeg46ngfr  40774  cdlemeg46req  40785  cdlemeg46gfv  40786  cdleme50trn1  40805  cdleme50trn2a  40806  cdlemf1  40817  cdlemf  40819  cdlemg10a  40896  cdlemg10  40897  cdlemg12d  40902  cdlemg12e  40903  cdlemg12f  40904  cdlemg12g  40905  cdlemg12  40906  cdlemg13  40908  cdlemg16ALTN  40914  cdlemg17b  40918  cdlemg17h  40924  cdlemg17pq  40928  cdlemg17iqN  40930  cdlemg17  40933  cdlemg19a  40939  cdlemg19  40940  cdlemg21  40942  cdlemg27a  40948  cdlemg27b  40952  cdlemg31c  40955  cdlemg33b0  40957  cdlemg33a  40962  cdlemg48  40993  tendocan  41080  cdlemk26-3  41162  cdlemk27-3  41163  cdlemk28-3  41164  cdlemk37  41170  cdlemky  41182  cdlemkyu  41183  cdlemk11ta  41185  cdlemkid3N  41189  cdlemk42  41197  cdlemk42yN  41200  cdlemk11t  41202  cdlemk45  41203  cdlemk46  41204  cdlemk47  41205  cdlemk51  41209  cdlemk52  41210  cdlemk53a  41211  cdleml4N  41235  dihord2pre2  41482  dihord4  41514  dihord5apre  41518  dihmeetlem1N  41546  dihmeetlem15N  41577  mapdpglem32  41961  mzpcong  43210  mullimc  45858  mullimcf  45865  addlimc  45888  iscnrm3rlem8  49188