Theorem simp21l 1289

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1196	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 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:  modexp  14273  segconeu  35992  4atlem10  39588  lplncvrlvol2  39597  4atex  40058  4atex2-0cOLDN  40062  cdlemd2  40181  cdlemd3  40182  cdlemd4  40183  cdleme0e  40199  cdleme0moN  40207  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme9  40235  cdleme11c  40243  cdleme11dN  40244  cdleme11e  40245  cdleme11fN  40246  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme11  40252  cdleme12  40253  cdleme13  40254  cdleme14  40255  cdleme15a  40256  cdleme15b  40257  cdleme15c  40258  cdleme15d  40259  cdleme15  40260  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme17d1  40271  cdleme18a  40273  cdleme18b  40274  cdleme18c  40275  cdleme18d  40277  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20c  40293  cdleme20d  40294  cdleme20e  40295  cdleme20f  40296  cdleme20g  40297  cdleme20h  40298  cdleme20j  40300  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme20  40306  cdleme21ct  40311  cdleme21e  40313  cdleme21i  40317  cdleme22aa  40321  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme26e  40341  cdleme27a  40349  cdleme32e  40427  cdlemg2fv2  40582  cdlemg4a  40590  cdlemg4d  40595  cdlemg4  40599  cdlemg6c  40602  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg9  40616  cdlemg12a  40625  cdlemg12c  40627  cdlemg17dALTN  40646  cdlemg17h  40650  cdlemg18b  40661  cdlemg18c  40662  cdlemg18d  40663  cdlemg18  40664  cdlemg19a  40665  cdlemg21  40668  cdlemg28a  40675  cdlemg31b0a  40677  cdlemg31d  40682  cdlemg33b0  40683  cdlemg33a  40688  cdlemh  40799  cdlemk5  40818  cdlemk6  40819  cdlemk7  40830  cdlemk11  40831  cdlemk12  40832  cdlemk21N  40855  cdlemk20  40856  cdlemk28-3  40890  cdlemk34  40892  cdlemkfid3N  40907  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk55u1  40947  cdlemn2  41177  cdlemn10  41188  dihjustlem  41198