Theorem simp21l 1281

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1188	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1125	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

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

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 1080

This theorem is referenced by:  modexp  13437  segconeu  33026  4atlem10  36223  lplncvrlvol2  36232  4atex  36693  4atex2-0cOLDN  36697  cdlemd2  36816  cdlemd3  36817  cdlemd4  36818  cdleme0e  36834  cdleme0moN  36842  cdleme3g  36851  cdleme3h  36852  cdleme3  36854  cdleme9  36870  cdleme11c  36878  cdleme11dN  36879  cdleme11e  36880  cdleme11fN  36881  cdleme11h  36883  cdleme11j  36884  cdleme11k  36885  cdleme11  36887  cdleme12  36888  cdleme13  36889  cdleme14  36890  cdleme15a  36891  cdleme15b  36892  cdleme15c  36893  cdleme15d  36894  cdleme15  36895  cdleme16b  36896  cdleme16c  36897  cdleme16d  36898  cdleme16e  36899  cdleme16f  36900  cdleme17d1  36906  cdleme18a  36908  cdleme18b  36909  cdleme18c  36910  cdleme18d  36912  cdleme19b  36921  cdleme19d  36923  cdleme19e  36924  cdleme20c  36928  cdleme20d  36929  cdleme20e  36930  cdleme20f  36931  cdleme20g  36932  cdleme20h  36933  cdleme20j  36935  cdleme20l2  36938  cdleme20l  36939  cdleme20m  36940  cdleme20  36941  cdleme21ct  36946  cdleme21e  36948  cdleme21i  36952  cdleme22aa  36956  cdleme22cN  36959  cdleme22d  36960  cdleme22e  36961  cdleme22eALTN  36962  cdleme22f  36963  cdleme26e  36976  cdleme27a  36984  cdleme32e  37062  cdlemg2fv2  37217  cdlemg4a  37225  cdlemg4d  37230  cdlemg4  37234  cdlemg6c  37237  cdlemg8b  37245  cdlemg8c  37246  cdlemg9a  37249  cdlemg9  37251  cdlemg12a  37260  cdlemg12c  37262  cdlemg17dALTN  37281  cdlemg17h  37285  cdlemg18b  37296  cdlemg18c  37297  cdlemg18d  37298  cdlemg18  37299  cdlemg19a  37300  cdlemg21  37303  cdlemg28a  37310  cdlemg31b0a  37312  cdlemg31d  37317  cdlemg33b0  37318  cdlemg33a  37323  cdlemh  37434  cdlemk5  37453  cdlemk6  37454  cdlemk7  37465  cdlemk11  37466  cdlemk12  37467  cdlemk21N  37490  cdlemk20  37491  cdlemk28-3  37525  cdlemk34  37527  cdlemkfid3N  37542  cdlemk35s-id  37555  cdlemk39s-id  37557  cdlemk55u1  37582  cdlemn2  37812  cdlemn10  37823  dihjustlem  37833