Theorem simp13l 1290

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

Assertion

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

Proof of Theorem simp13l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pceu  16786  axpasch  29026  3atlem4  39856  llncvrlpln2  39927  2lplnja  39989  2lnat  40154  llnexchb2  40239  lhp2lt  40371  lhpmcvr5N  40397  4atexlemq  40421  4atexlemex6  40444  trlval2  40533  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme11l  40639  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15b  40645  cdleme15  40648  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme18d  40665  cdleme19b  40674  cdleme19e  40677  cdleme20d  40682  cdleme20g  40685  cdleme20h  40686  cdleme20i  40687  cdleme20j  40688  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21d  40700  cdleme21e  40701  cdleme21h  40704  cdleme22f  40716  cdleme23a  40719  cdleme23b  40720  cdleme23c  40721  cdleme24  40722  cdleme25a  40723  cdleme25dN  40726  cdleme26ee  40730  cdleme26fALTN  40732  cdleme26f  40733  cdleme26f2ALTN  40734  cdleme26f2  40735  cdleme27a  40737  cdlemefr29bpre0N  40776  cdlemefr29clN  40777  cdlemefr32fvaN  40779  cdlemefr32fva1  40780  cdleme41sn3a  40803  cdleme35a  40818  cdleme35fnpq  40819  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35f  40824  cdleme36m  40831  cdleme37m  40832  cdleme39n  40836  cdleme43bN  40860  cdleme43dN  40862  cdleme17d2  40865  cdlemeg46c  40883  cdlemeg46nlpq  40887  cdlemeg46ngfr  40888  cdlemeg46req  40899  cdlemeg46gfv  40900  cdleme50trn1  40919  cdleme50trn2a  40920  cdlemf1  40931  cdlemf  40933  cdlemg10a  41010  cdlemg10  41011  cdlemg12d  41016  cdlemg12e  41017  cdlemg12f  41018  cdlemg12g  41019  cdlemg12  41020  cdlemg13  41022  cdlemg16ALTN  41028  cdlemg17b  41032  cdlemg17h  41038  cdlemg17pq  41042  cdlemg17iqN  41044  cdlemg17  41047  cdlemg19a  41053  cdlemg19  41054  cdlemg21  41056  cdlemg27a  41062  cdlemg27b  41066  cdlemg31c  41069  cdlemg33b0  41071  cdlemg33a  41076  cdlemg48  41107  tendocan  41194  cdlemk26-3  41276  cdlemk27-3  41277  cdlemk28-3  41278  cdlemk37  41284  cdlemky  41296  cdlemkyu  41297  cdlemk11ta  41299  cdlemkid3N  41303  cdlemk42  41311  cdlemk42yN  41314  cdlemk11t  41316  cdlemk45  41317  cdlemk46  41318  cdlemk47  41319  cdlemk51  41323  cdlemk52  41324  cdlemk53a  41325  cdleml4N  41349  dihord2pre2  41596  dihord4  41628  dihord5apre  41632  dihmeetlem1N  41660  dihmeetlem15N  41691  mapdpglem32  42075  mzpcong  43323  mullimc  45970  mullimcf  45977  addlimc  46000  iscnrm3rlem8  49300