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  16931  axpasch  29328  3atlem4  40301  llncvrlpln2  40372  2lplnja  40434  2lnat  40599  llnexchb2  40684  lhp2lt  40816  lhpmcvr5N  40842  4atexlemq  40866  4atexlemex6  40889  trlval2  40978  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11l  41084  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15b  41090  cdleme15  41093  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme18d  41110  cdleme19b  41119  cdleme19e  41122  cdleme20d  41127  cdleme20g  41130  cdleme20h  41131  cdleme20i  41132  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21d  41145  cdleme21e  41146  cdleme21h  41149  cdleme22f  41161  cdleme23a  41164  cdleme23b  41165  cdleme23c  41166  cdleme24  41167  cdleme25a  41168  cdleme25dN  41171  cdleme26ee  41175  cdleme26fALTN  41177  cdleme26f  41178  cdleme26f2ALTN  41179  cdleme26f2  41180  cdleme27a  41182  cdlemefr29bpre0N  41221  cdlemefr29clN  41222  cdlemefr32fvaN  41224  cdlemefr32fva1  41225  cdleme41sn3a  41248  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35f  41269  cdleme36m  41276  cdleme37m  41277  cdleme39n  41281  cdleme43bN  41305  cdleme43dN  41307  cdleme17d2  41310  cdlemeg46c  41328  cdlemeg46nlpq  41332  cdlemeg46ngfr  41333  cdlemeg46req  41344  cdlemeg46gfv  41345  cdleme50trn1  41364  cdleme50trn2a  41365  cdlemf1  41376  cdlemf  41378  cdlemg10a  41455  cdlemg10  41456  cdlemg12d  41461  cdlemg12e  41462  cdlemg12f  41463  cdlemg12g  41464  cdlemg12  41465  cdlemg13  41467  cdlemg16ALTN  41473  cdlemg17b  41477  cdlemg17h  41483  cdlemg17pq  41487  cdlemg17iqN  41489  cdlemg17  41492  cdlemg19a  41498  cdlemg19  41499  cdlemg21  41501  cdlemg27a  41507  cdlemg27b  41511  cdlemg31c  41514  cdlemg33b0  41516  cdlemg33a  41521  cdlemg48  41552  tendocan  41639  cdlemk26-3  41721  cdlemk27-3  41722  cdlemk28-3  41723  cdlemk37  41729  cdlemky  41741  cdlemkyu  41742  cdlemk11ta  41744  cdlemkid3N  41748  cdlemk42  41756  cdlemk42yN  41759  cdlemk11t  41761  cdlemk45  41762  cdlemk46  41763  cdlemk47  41764  cdlemk51  41768  cdlemk52  41769  cdlemk53a  41770  cdleml4N  41794  dihord2pre2  42041  dihord4  42073  dihord5apre  42077  dihmeetlem1N  42105  dihmeetlem15N  42136  mapdpglem32  42520  mzpcong  43740  mullimc  46373  mullimcf  46380  addlimc  46403  iscnrm3rlem8  49766